Theorem atcvat4 10324

Description: A condition implying existence of an atom with the properties shown. Lemma 3.2.20 of [PtakPulmannova] p. 68.

Hypothesis

Ref	Expression
atcvat3.1	|- A e. CH

Assertion

Ref	Expression
atcvat4	|- ((B e. Atoms /\ C e. Atoms) -> ((A =/= 0H /\ B (_ (A vH C)) -> E.x e. Atoms (x (_ A /\ B (_ (C vH x))))

Distinct variable groups:   x,A   x,B   x,C

Proof of Theorem atcvat4

Step	Hyp	Ref	Expression
1		sseq1 2082	. . . . . . . . . . . . . . 15 |- (B = C -> (B (_ (C vH x) <-> C (_ (C vH x)))
2		chub1t 9430	. . . . . . . . . . . . . . . 16 |- ((C e. CH /\ x e. CH) -> C (_ (C vH x))
3		atelch 10271	. . . . . . . . . . . . . . . 16 |- (C e. Atoms -> C e. CH)
4		atelch 10271	. . . . . . . . . . . . . . . 16 |- (x e. Atoms -> x e. CH)
5	2, 3, 4	syl2an 454	. . . . . . . . . . . . . . 15 |- ((C e. Atoms /\ x e. Atoms) -> C (_ (C vH x))
6	1, 5	syl5bir 210	. . . . . . . . . . . . . 14 |- (B = C -> ((C e. Atoms /\ x e. Atoms) -> B (_ (C vH x)))
7	6	exp3a 375	. . . . . . . . . . . . 13 |- (B = C -> (C e. Atoms -> (x e. Atoms -> B (_ (C vH x))))
8	7	impcom 351	. . . . . . . . . . . 12 |- ((C e. Atoms /\ B = C) -> (x e. Atoms -> B (_ (C vH x)))
9	8	anim2d 561	. . . . . . . . . . 11 |- ((C e. Atoms /\ B = C) -> ((x (_ A /\ x e. Atoms) -> (x (_ A /\ B (_ (C vH x))))
10	9	exp3a 375	. . . . . . . . . 10 |- ((C e. Atoms /\ B = C) -> (x (_ A -> (x e. Atoms -> (x (_ A /\ B (_ (C vH x)))))
11	10	com23 32	. . . . . . . . 9 |- ((C e. Atoms /\ B = C) -> (x e. Atoms -> (x (_ A -> (x (_ A /\ B (_ (C vH x)))))
12	11	r19.22dv 1737	. . . . . . . 8 |- ((C e. Atoms /\ B = C) -> (E.x e. Atoms x (_ A -> E.x e. Atoms (x (_ A /\ B (_ (C vH x))))
13		atcvat3.1	. . . . . . . . 9 |- A e. CH
14	13	hatomic 10286	. . . . . . . 8 |- (A =/= 0H -> E.x e. Atoms x (_ A)
15	12, 14	syl5 21	. . . . . . 7 |- ((C e. Atoms /\ B = C) -> (A =/= 0H -> E.x e. Atoms (x (_ A /\ B (_ (C vH x))))
16	15	ex 373	. . . . . 6 |- (C e. Atoms -> (B = C -> (A =/= 0H -> E.x e. Atoms (x (_ A /\ B (_ (C vH x)))))
17	16	a1i 8	. . . . 5 |- (B (_ (A vH C) -> (C e. Atoms -> (B = C -> (A =/= 0H -> E.x e. Atoms (x (_ A /\ B (_ (C vH x))))))
18	17	com4l 39	. . . 4 |- (C e. Atoms -> (B = C -> (A =/= 0H -> (B (_ (A vH C) -> E.x e. Atoms (x (_ A /\ B (_ (C vH x))))))
19	18	imp4a 364	. . 3 |- (C e. Atoms -> (B = C -> ((A =/= 0H /\ B (_ (A vH C)) -> E.x e. Atoms (x (_ A /\ B (_ (C vH x)))))
20	19	adantl 388	. 2 |- ((B e. Atoms /\ C e. Atoms) -> (B = C -> ((A =/= 0H /\ B (_ (A vH C)) -> E.x e. Atoms (x (_ A /\ B (_ (C vH x)))))
21		chlejb2t 9436	. . . . . . . . . . . . . . . . 17 |- ((C e. CH /\ A e. CH) -> (C (_ A <-> (A vH C) = A))
22	13, 21	mpan2 696	. . . . . . . . . . . . . . . 16 |- (C e. CH -> (C (_ A <-> (A vH C) = A))
23	22	biimpa 416	. . . . . . . . . . . . . . 15 |- ((C e. CH /\ C (_ A) -> (A vH C) = A)
24	23	sseq2d 2089	. . . . . . . . . . . . . 14 |- ((C e. CH /\ C (_ A) -> (B (_ (A vH C) <-> B (_ A))
25	24	biimpa 416	. . . . . . . . . . . . 13 |- (((C e. CH /\ C (_ A) /\ B (_ (A vH C)) -> B (_ A)
26	25	anasss 440	. . . . . . . . . . . 12 |- ((C e. CH /\ (C (_ A /\ B (_ (A vH C))) -> B (_ A)
27	26	ex 373	. . . . . . . . . . 11 |- (C e. CH -> ((C (_ A /\ B (_ (A vH C)) -> B (_ A))
28	27	adantl 388	. . . . . . . . . 10 |- ((B e. CH /\ C e. CH) -> ((C (_ A /\ B (_ (A vH C)) -> B (_ A))
29		chub2t 9431	. . . . . . . . . 10 |- ((B e. CH /\ C e. CH) -> B (_ (C vH B))
30	28, 29	jctird 602	. . . . . . . . 9 |- ((B e. CH /\ C e. CH) -> ((C (_ A /\ B (_ (A vH C)) -> (B (_ A /\ B (_ (C vH B))))
31		atelch 10271	. . . . . . . . 9 |- (B e. Atoms -> B e. CH)
32	30, 31, 3	syl2an 454	. . . . . . . 8 |- ((B e. Atoms /\ C e. Atoms) -> ((C (_ A /\ B (_ (A vH C)) -> (B (_ A /\ B (_ (C vH B))))
33		pm3.26 319	. . . . . . . 8 |- ((B e. Atoms /\ C e. Atoms) -> B e. Atoms)
34	32, 33	jctild 601	. . . . . . 7 |- ((B e. Atoms /\ C e. Atoms) -> ((C (_ A /\ B (_ (A vH C)) -> (B e. Atoms /\ (B (_ A /\ B (_ (C vH B)))))
35	34	imp 350	. . . . . 6 |- (((B e. Atoms /\ C e. Atoms) /\ (C (_ A /\ B (_ (A vH C))) -> (B e. Atoms /\ (B (_ A /\ B (_ (C vH B))))
36	35	anassrs 441	. . . . 5 |- ((((B e. Atoms /\ C e. Atoms) /\ C (_ A) /\ B (_ (A vH C)) -> (B e. Atoms /\ (B (_ A /\ B (_ (C vH B))))
37		sseq1 2082	. . . . . . 7 |- (x = B -> (x (_ A <-> B (_ A))
38		opreq2 3969	. . . . . . . 8 |- (x = B -> (C vH x) = (C vH B))
39	38	sseq2d 2089	. . . . . . 7 |- (x = B -> (B (_ (C vH x) <-> B (_ (C vH B)))
40	37, 39	anbi12d 628	. . . . . 6 |- (x = B -> ((x (_ A /\ B (_ (C vH x)) <-> (B (_ A /\ B (_ (C vH B))))
41	40	rcla4ev 1877	. . . . 5 |- ((B e. Atoms /\ (B (_ A /\ B (_ (C vH B))) -> E.x e. Atoms (x (_ A /\ B (_ (C vH x)))
42	36, 41	syl 10	. . . 4 |- ((((B e. Atoms /\ C e. Atoms) /\ C (_ A) /\ B (_ (A vH C)) -> E.x e. Atoms (x (_ A /\ B (_ (C vH x)))
43	42	adantrl 394	. . 3 |- ((((B e. Atoms /\ C e. Atoms) /\ C (_ A) /\ (A =/= 0H /\ B (_ (A vH C))) -> E.x e. Atoms (x (_ A /\ B (_ (C vH x)))
44	43	exp31 376	. 2 |- ((B e. Atoms /\ C e. Atoms) -> (C (_ A -> ((A =/= 0H /\ B (_ (A vH C)) -> E.x e. Atoms (x (_ A /\ B (_ (C vH x)))))
45	13	atcvat3 10323	. . . . . . 7 |- ((B e. Atoms /\ C e. Atoms) -> (((-. B = C /\ -. C (_ A) /\ B (_ (A vH C)) -> (A i^i (B vH C)) e. Atoms))
46		atexcht 10308	. . . . . . . . . 10 |- ((C e. CH /\ (A i^i (B vH C)) e. Atoms /\ B e. Atoms) -> (((A i^i (B vH C)) (_ (C vH B) /\ (C i^i (A i^i (B vH C))) = 0H) -> B (_ (C vH (A i^i (B vH C)))))
47	3	ad2antlr 405	. . . . . . . . . . 11 |- (((B e. Atoms /\ C e. Atoms) /\ ((-. B = C /\ -. C (_ A) /\ B (_ (A vH C))) -> C e. CH)
48	45	imp 350	. . . . . . . . . . 11 |- (((B e. Atoms /\ C e. Atoms) /\ ((-. B = C /\ -. C (_ A) /\ B (_ (A vH C))) -> (A i^i (B vH C)) e. Atoms)
49		simpll 412	. . . . . . . . . . 11 |- (((B e. Atoms /\ C e. Atoms) /\ ((-. B = C /\ -. C (_ A) /\ B (_ (A vH C))) -> B e. Atoms)
50	47, 48, 49	3jca 819	. . . . . . . . . 10 |- (((B e. Atoms /\ C e. Atoms) /\ ((-. B = C /\ -. C (_ A) /\ B (_ (A vH C))) -> (C e. CH /\ (A i^i (B vH C)) e. Atoms /\ B e. Atoms))
51		inss2 2231	. . . . . . . . . . . . . 14 |- (A i^i (B vH C)) (_ (B vH C)
52	51	a1i 8	. . . . . . . . . . . . 13 |- ((B e. Atoms /\ C e. Atoms) -> (A i^i (B vH C)) (_ (B vH C))
53		chjcomt 9429	. . . . . . . . . . . . . 14 |- ((B e. CH /\ C e. CH) -> (B vH C) = (C vH B))
54	53, 31, 3	syl2an 454	. . . . . . . . . . . . 13 |- ((B e. Atoms /\ C e. Atoms) -> (B vH C) = (C vH B))
55	52, 54	sseqtrd 2097	. . . . . . . . . . . 12 |- ((B e. Atoms /\ C e. Atoms) -> (A i^i (B vH C)) (_ (C vH B))
56	55	adantr 389	. . . . . . . . . . 11 |- (((B e. Atoms /\ C e. Atoms) /\ ((-. B = C /\ -. C (_ A) /\ B (_ (A vH C))) -> (A i^i (B vH C)) (_ (C vH B))
57		atnssm0 10303	. . . . . . . . . . . . . . . . 17 |- ((A e. CH /\ C e. Atoms) -> (-. C (_ A <-> (A i^i C) = 0H))
58	13, 57	mpan 695	. . . . . . . . . . . . . . . 16 |- (C e. Atoms -> (-. C (_ A <-> (A i^i C) = 0H))
59	58	adantl 388	. . . . . . . . . . . . . . 15 |- ((B e. Atoms /\ C e. Atoms) -> (-. C (_ A <-> (A i^i C) = 0H))
60		chinclt 9422	. . . . . . . . . . . . . . . . . . 19