Theorem atcvat4 5775

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 group(s):   x,A   x,B   x,C

Proof of Theorem atcvat4

Step	Hyp	Ref	Expression
1		sseq1 1521	. . . . . . . . . . . . . . . 16 |- (B = C -> (B (_ (C vH x) <-> C (_ (C vH x)))
2		chub1t 5424	. . . . . . . . . . . . . . . . 17 |- ((C e. CH /\ x e. CH) -> C (_ (C vH x))
3		atelch 5742	. . . . . . . . . . . . . . . . 17 |- (C e. Atoms -> C e. CH)
4		atelch 5742	. . . . . . . . . . . . . . . . 17 |- (x e. Atoms -> x e. CH)
5	2, 3, 4	syl2an 349	. . . . . . . . . . . . . . . 16 |- ((C e. Atoms /\ x e. Atoms) -> C (_ (C vH x))
6	1, 5	syl5bir 184	. . . . . . . . . . . . . . 15 |- (B = C -> ((C e. Atoms /\ x e. Atoms) -> B (_ (C vH x)))
7	6	exp3a 292	. . . . . . . . . . . . . 14 |- (B = C -> (C e. Atoms -> (x e. Atoms -> B (_ (C vH x))))
8	7	com12 13	. . . . . . . . . . . . 13 |- (C e. Atoms -> (B = C -> (x e. Atoms -> B (_ (C vH x))))
9	8	imp 277	. . . . . . . . . . . 12 |- ((C e. Atoms /\ B = C) -> (x e. Atoms -> B (_ (C vH x)))
10	9	anim2d 433	. . . . . . . . . . 11 |- ((C e. Atoms /\ B = C) -> ((x (_ A /\ x e. Atoms) -> (x (_ A /\ B (_ (C vH x))))
11	10	exp3a 292	. . . . . . . . . 10 |- ((C e. Atoms /\ B = C) -> (x (_ A -> (x e. Atoms -> (x (_ A /\ B (_ (C vH x)))))
12	11	com23 32	. . . . . . . . 9 |- ((C e. Atoms /\ B = C) -> (x e. Atoms -> (x (_ A -> (x (_ A /\ B (_ (C vH x)))))
13	12	r19.22dv 1278	. . . . . . . 8 |- ((C e. Atoms /\ B = C) -> (E.x e. Atoms x (_ A -> E.x e. Atoms (x (_ A /\ B (_ (C vH x))))
14		atcvat3.1	. . . . . . . . 9 |- A e. CH
15	14	hatomic 5754	. . . . . . . 8 |- (-. A = 0H -> E.x e. Atoms x (_ A)
16	13, 15	syl5 22	. . . . . . 7 |- ((C e. Atoms /\ B = C) -> (-. A = 0H -> E.x e. Atoms (x (_ A /\ B (_ (C vH x))))
17	16	exp 291	. . . . . 6 |- (C e. Atoms -> (B = C -> (-. A = 0H -> E.x e. Atoms (x (_ A /\ B (_ (C vH x)))))
18	17	a1i 7	. . . . 5 |- (B (_ (A vH C) -> (C e. Atoms -> (B = C -> (-. A = 0H -> E.x e. Atoms (x (_ A /\ B (_ (C vH x))))))
19	18	com4l 39	. . . 4 |- (C e. Atoms -> (B = C -> (-. A = 0H -> (B (_ (A vH C) -> E.x e. Atoms (x (_ A /\ B (_ (C vH x))))))
20	19	imp4a 282	. . 3 |- (C e. Atoms -> (B = C -> ((-. A = 0H /\ B (_ (A vH C)) -> E.x e. Atoms (x (_ A /\ B (_ (C vH x)))))
21	20	adantl 305	. 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)))))
22		pm3.26 256	. . . . . . . . 9 |- ((B e. Atoms /\ C e. Atoms) -> B e. Atoms)
23	22	a1d 14	. . . . . . . 8 |- ((B e. Atoms /\ C e. Atoms) -> ((C (_ A /\ B (_ (A vH C)) -> B e. Atoms))
24		chlejb2t 5430	. . . . . . . . . . . . . . . . 17 |- ((C e. CH /\ A e. CH) -> (C (_ A <-> (A vH C) = A))
25	14, 24	mpan2 519	. . . . . . . . . . . . . . . 16 |- (C e. CH -> (C (_ A <-> (A vH C) = A))
26	25	biimpa 324	. . . . . . . . . . . . . . 15 |- ((C e. CH /\ C (_ A) -> (A vH C) = A)
27	26	sseq2d 1528	. . . . . . . . . . . . . 14 |- ((C e. CH /\ C (_ A) -> (B (_ (A vH C) <-> B (_ A))
28	27	biimpa 324	. . . . . . . . . . . . 13 |- (((C e. CH /\ C (_ A) /\ B (_ (A vH C)) -> B (_ A)
29	28	anasss 337	. . . . . . . . . . . 12 |- ((C e. CH /\ (C (_ A /\ B (_ (A vH C))) -> B (_ A)
30	29	exp 291	. . . . . . . . . . 11 |- (C e. CH -> ((C (_ A /\ B (_ (A vH C)) -> B (_ A))
31	30	adantl 305	. . . . . . . . . 10 |- ((B e. CH /\ C e. CH) -> ((C (_ A /\ B (_ (A vH C)) -> B (_ A))
32		chub2t 5425	. . . . . . . . . . 11 |- ((B e. CH /\ C e. CH) -> B (_ (C vH B))
33	32	a1d 14	. . . . . . . . . 10 |- ((B e. CH /\ C e. CH) -> ((C (_ A /\ B (_ (A vH C)) -> B (_ (C vH B)))
34	31, 33	jcad 455	. . . . . . . . 9 |- ((B e. CH /\ C e. CH) -> ((C (_ A /\ B (_ (A vH C)) -> (B (_ A /\ B (_ (C vH B))))
35		atelch 5742	. . . . . . . . 9 |- (B e. Atoms -> B e. CH)
36	34, 35, 3	syl2an 349	. . . . . . . 8 |- ((B e. Atoms /\ C e. Atoms) -> ((C (_ A /\ B (_ (A vH C)) -> (B (_ A /\ B (_ (C vH B))))
37	23, 36	jcad 455	. . . . . . 7 |- ((B e. Atoms /\ C e. Atoms) -> ((C (_ A /\ B (_ (A vH C)) -> (B e. Atoms /\ (B (_ A /\ B (_ (C vH B)))))
38	37	imp 277	. . . . . 6 |- (((B e. Atoms /\ C e. Atoms) /\ (C (_ A /\ B (_ (A vH C))) -> (B e. Atoms /\ (B (_ A /\ B (_ (C vH B))))
39	38	anassrs 338	. . . . 5 |- ((((B e. Atoms /\ C e. Atoms) /\ C (_ A) /\ B (_ (A vH C)) -> (B e. Atoms /\ (B (_ A /\ B (_ (C vH B))))
40		sseq1 1521	. . . . . . 7 |- (x = B -> (x (_ A <-> B (_ A))
41		opreq2 3007	. . . . . . . 8 |- (x = B -> (C vH x) = (C vH B))
42	41	sseq2d 1528	. . . . . . 7 |- (x = B -> (B (_ (C vH x) <-> B (_ (C vH B)))
43	40, 42	anbi12d 476	. . . . . 6 |- (x = B -> ((x (_ A /\ B (_ (C vH x)) <-> (B (_ A /\ B (_ (C vH B))))
44	43	rcla4ev 1403	. . . . 5 |- ((B e. Atoms /\ (B (_ A /\ B (_ (C vH B))) -> E.x e. Atoms (x (_ A /\ B (_ (C vH x)))
45	39, 44	syl 12	. . . 4 |- ((((B e. Atoms /\ C e. Atoms) /\ C (_ A) /\ B (_ (A vH C)) -> E.x e. Atoms (x (_ A /\ B (_ (C vH x)))
46	45	adantrl 311	. . 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)))
47	46	exp31 293	. 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)))))
48	14	atcvat3 5774	. . . . . . 7 |- ((B e. Atoms /\ C e. Atoms) -> (((-. B = C /\ -. C (_ A) /\ B (_ (A vH C)) -> (A i^i (B vH C)) e. Atoms))
49		atexch 5769	. . . . . . . . . 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)))))
50	3	ad2antlr 321	. . . . . . . . . . 11 |- (((B e. Atoms /\ C e. Atoms) /\ ((-. B = C /\ -. C (_ A) /\ B (_ (A vH C))) -> C e. CH)
51	48	imp 277	. . . . . . . . . . 11 |- (((B e. Atoms /\ C e. Atoms) /\ ((-. B = C /\ -. C (_ A) /\ B (_ (A vH C))) -> (A i^i (B vH C)) e. Atoms)
52	22	adantr 306	. . . . . . . . . . 11 |- (((B e. Atoms /\ C e. Atoms) /\ ((-. B = C /\ -. C (_ A) /\ B (_ (A vH C))) -> B e. Atoms)
53	50, 51, 52	3jca 604	. . . . . . . . . 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))
54		inss2 1658	. . . . . . . . . . . . . 14 |- (A i^i (B vH C)) (_ (B vH C)
55	54	a1i 7	. . . . . . . . . . . . 13 |- ((B e. Atoms /\ C e. Atoms) -> (A i^i (B vH C)) (_ (B vH C))
56		chjcomt 5423	. . . . . . . . . . . . . 14 |- ((B e. CH /\ C e. CH) -> (B vH C) = (C vH B))
57	56, 35, 3	syl2an 349	. . . . . . . . . . . . 13 |- ((B e. Atoms /\ C e. Atoms) -> (B vH C) = (C vH B))
58	55, 57	sseqtrd 1536	. . . . . . . . . . . 12 |- ((B e. Atoms /\ C e. Atoms) -> (A i^i (B vH C)) (_ (C vH B))
59	58	adantr 306	. . . . . . . . . . 11 |- (((B e. Atoms /\ C e. Atoms) /\ ((-. B = C /\ -. C (_ A) /\ B (_ (A vH C))) -> (A i^i (B vH C)) (_ (C vH B))
60		atnssm0 5765	. . . . . . . . . . . . . . . . 17 |- ((A e. CH /\ C e. Atoms) -> (-. C (_ A <-> (A i^i C) = 0H))
61	14, 60	mpan 518	. . . . . . . . . . . . . . . 16 |- (C e. Atoms -> (-. C (_