Theorem atcvatlem 5770

Description: Lemma for atcvat 5771.

Hypothesis

Ref	Expression
atoml.1	⊢ A ∈ Cℋ

Assertion

Ref	Expression
atcvatlem	⊢ (((B ∈ Atoms ∧ C ∈ Atoms) ∧ (¬ A = 0ℋ ∧ A ⊂ (B ∨ℋ C))) → (¬ B ⊆ A → A ∈ Atoms))

76

Proof of Theorem atcvatlem

Step	Hyp	Ref	Expression
1		atnem0 5766	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ Atoms ∧ B ∈ Atoms) → (¬ x = B ↔ (x ∩ B) = 0ℋ))
2		sseq1 1521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = B → (x ⊆ A ↔ B ⊆ A))
3	2	biimpcd 137	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x ⊆ A → (x = B → B ⊆ A))
4	3	con3d 87	. . . . . . . . . . . . . . . . . . 19 ⊢ (x ⊆ A → (¬ B ⊆ A → ¬ x = B))
5	4	imp 277	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ⊆ A ∧ ¬ B ⊆ A) → ¬ x = B)
6	5	adantrl 311	. . . . . . . . . . . . . . . . 17 ⊢ ((x ⊆ A ∧ (A ⊂ (B ∨ℋ C) ∧ ¬ B ⊆ A)) → ¬ x = B)
7	1, 6	syl5bi 183	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ Atoms ∧ B ∈ Atoms) → ((x ⊆ A ∧ (A ⊂ (B ∨ℋ C) ∧ ¬ B ⊆ A)) → (x ∩ B) = 0ℋ))
8		cvp 5764	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∈ Cℋ ∧ B ∈ Atoms) → ((x ∩ B) = 0ℋ ↔ x ⋖ (x ∨ℋ B)))
9		chjcomt 5423	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((x ∈ Cℋ ∧ B ∈ Cℋ ) → (x ∨ℋ B) = (B ∨ℋ x))
10		atelch 5742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (B ∈ Atoms → B ∈ Cℋ )
11	9, 10	sylan2 346	. . . . . . . . . . . . . . . . . . 19 ⊢ ((x ∈ Cℋ ∧ B ∈ Atoms) → (x ∨ℋ B) = (B ∨ℋ x))
12	11	breq2d 2072	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∈ Cℋ ∧ B ∈ Atoms) → (x ⋖ (x ∨ℋ B) ↔ x ⋖ (B ∨ℋ x)))
13	8, 12	bitrd 406	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ Cℋ ∧ B ∈ Atoms) → ((x ∩ B) = 0ℋ ↔ x ⋖ (B ∨ℋ x)))
14		atelch 5742	. . . . . . . . . . . . . . . . 17 ⊢ (x ∈ Atoms → x ∈ Cℋ )
15	13, 14	sylan 343	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ Atoms ∧ B ∈ Atoms) → ((x ∩ B) = 0ℋ ↔ x ⋖ (B ∨ℋ x)))
16	7, 15	sylibd 177	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ Atoms ∧ B ∈ Atoms) → ((x ⊆ A ∧ (A ⊂ (B ∨ℋ C) ∧ ¬ B ⊆ A)) → x ⋖ (B ∨ℋ x)))
17	16	ancoms 334	. . . . . . . . . . . . . 14 ⊢ ((B ∈ Atoms ∧ x ∈ Atoms) → ((x ⊆ A ∧ (A ⊂ (B ∨ℋ C) ∧ ¬ B ⊆ A)) → x ⋖ (B ∨ℋ x)))
18	17	adantlr 310	. . . . . . . . . . . . 13 ⊢ (((B ∈ Atoms ∧ C ∈ Atoms) ∧ x ∈ Atoms) → ((x ⊆ A ∧ (A ⊂ (B ∨ℋ C) ∧ ¬ B ⊆ A)) → x ⋖ (B ∨ℋ x)))
19	18	imp 277	. . . . . . . . . . . 12 ⊢ ((((B ∈ Atoms ∧ C ∈ Atoms) ∧ x ∈ Atoms) ∧ (x ⊆ A ∧ (A ⊂ (B ∨ℋ C) ∧ ¬ B ⊆ A))) → x ⋖ (B ∨ℋ x))
20		chub1t 5424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((B ∈ Cℋ ∧ x ∈ Cℋ ) → B ⊆ (B ∨ℋ x))
21	20, 10, 14	syl2an 349	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((B ∈ Atoms ∧ x ∈ Atoms) → B ⊆ (B ∨ℋ x))
22	21	3adant3 599	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) → B ⊆ (B ∨ℋ x))
23	22	adantr 306	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ ((x ⊆ A ∧ ¬ B ⊆ A) ∧ A ⊂ (B ∨ℋ C))) → B ⊆ (B ∨ℋ x))
24		sstr 1511	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((x ⊆ A ∧ A ⊆ (B ∨ℋ C)) → x ⊆ (B ∨ℋ C))
25		pssss 1567	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (A ⊂ (B ∨ℋ C) → A ⊆ (B ∨ℋ C))
26	24, 25	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((x ⊆ A ∧ A ⊂ (B ∨ℋ C)) → x ⊆ (B ∨ℋ C))
27	26	adantlr 310	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((x ⊆ A ∧ ¬ B ⊆ A) ∧ A ⊂ (B ∨ℋ C)) → x ⊆ (B ∨ℋ C))
28	27	adantl 305	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ ((x ⊆ A ∧ ¬ B ⊆ A) ∧ A ⊂ (B ∨ℋ C))) → x ⊆ (B ∨ℋ C))
29	1, 5	syl5bi 183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((x ∈ Atoms ∧ B ∈ Atoms) → ((x ⊆ A ∧ ¬ B ⊆ A) → (x ∩ B) = 0ℋ))
30	29	ancoms 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((B ∈ Atoms ∧ x ∈ Atoms) → ((x ⊆ A ∧ ¬ B ⊆ A) → (x ∩ B) = 0ℋ))
31	30	3adant3 599	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) → ((x ⊆ A ∧ ¬ B ⊆ A) → (x ∩ B) = 0ℋ))
32	31	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ (x ⊆ A ∧ ¬ B ⊆ A)) → (x ∩ B) = 0ℋ)
33		incom 1636	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (B ∩ x) = (x ∩ B)
34	32, 33	syl5eq 1136	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ (x ⊆ A ∧ ¬ B ⊆ A)) → (B ∩ x) = 0ℋ)
35	34	adantrr 312	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ ((x ⊆ A ∧ ¬ B ⊆ A) ∧ A ⊂ (B ∨ℋ C))) → (B ∩ x) = 0ℋ)
36		atexch 5769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((B ∈ Cℋ ∧ x ∈ Atoms ∧ C ∈ Atoms) → ((x ⊆ (B ∨ℋ C) ∧ (B ∩ x) = 0ℋ) → C ⊆ (B ∨ℋ x)))
37	36, 10	syl3an1 619	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) → ((x ⊆ (B ∨ℋ C) ∧ (B ∩ x) = 0ℋ) → C ⊆ (B ∨ℋ x)))
38	37	adantr 306	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ ((x ⊆ A ∧ ¬ B ⊆ A) ∧ A ⊂ (B ∨ℋ C))) → ((x ⊆ (B ∨ℋ C) ∧ (B ∩ x) = 0ℋ) → C ⊆ (B ∨ℋ x)))
39	28, 35, 38	mp2and 526	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ ((x ⊆ A ∧ ¬ B ⊆ A) ∧ A ⊂ (B ∨ℋ C))) → C ⊆ (B ∨ℋ x))
40	23, 39	jca 236	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ ((x ⊆ A ∧ ¬ B ⊆ A) ∧ A ⊂ (B ∨ℋ C))) → (B ⊆ (B ∨ℋ x) ∧ C ⊆ (B ∨ℋ x)))
41		3simp1 594	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((B ∈ Cℋ ∧ x ∈ Cℋ ∧ C ∈ Cℋ ) → B ∈ Cℋ )
42		3simp3 596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((B ∈ Cℋ ∧ x ∈ Cℋ ∧ C ∈ Cℋ ) → C ∈ Cℋ )
43		chjclt 5330	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((B ∈ Cℋ ∧ x ∈ Cℋ ) → (B ∨ℋ x) ∈ Cℋ )
44	43	3adant3 599	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((B ∈ Cℋ ∧ x ∈ Cℋ ∧ C ∈ Cℋ ) → (B ∨ℋ x) ∈ Cℋ )
45	41, 42, 44	3jca 604	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((B ∈ Cℋ ∧ x ∈ Cℋ ∧ C ∈ Cℋ ) → (B ∈ Cℋ ∧ C ∈ Cℋ ∧ (B ∨ℋ x) ∈ Cℋ ))
46		atelch 5742	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (C ∈ Atoms → C ∈ Cℋ )
47	45, 10, 14, 46	syl3an 628	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) → (B ∈ Cℋ ∧ C ∈ Cℋ ∧ (B ∨ℋ x) ∈ Cℋ ))
48		chlubt 5426	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((B ∈ Cℋ ∧ C ∈ Cℋ ∧ (B ∨ℋ x) ∈ Cℋ ) → ((B ⊆ (B ∨ℋ x) ∧ C ⊆ (B ∨ℋ x)) ↔ (B ∨ℋ C) ⊆ (B ∨ℋ x)))
49	47, 48	syl 12	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) → ((B ⊆ (B ∨ℋ x) ∧ C ⊆ (B ∨ℋ x)) ↔ (B ∨ℋ C) ⊆ (B ∨ℋ x)))
50	49	adantr 306	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ ((x ⊆ A ∧ ¬ B ⊆ A) ∧ A ⊂ (B ∨ℋ C))) → ((B ⊆ (B ∨ℋ x) ∧ C ⊆ (B ∨ℋ x)) ↔ (B ∨ℋ C) ⊆ (B ∨ℋ x)))
51	40, 50	mpbid 170	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ ((x ⊆ A ∧ ¬ B ⊆ A) ∧ A ⊂ (B ∨ℋ C))) → (B ∨ℋ C) ⊆ (B ∨ℋ x))
52		chub1t 5424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((B ∈ Cℋ ∧ C ∈ Cℋ ) → B ⊆ (B ∨ℋ C))
53	52	3adant2 598	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((B ∈ Cℋ ∧ x ∈ Cℋ ∧ C ∈ Cℋ ) → B ⊆ (B ∨ℋ C))
54	53, 27	anim12i 268	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((B ∈ Cℋ ∧ x ∈ Cℋ ∧ C ∈ Cℋ ) ∧ ((x ⊆ A ∧ ¬ B ⊆ A) ∧ A ⊂ (B ∨ℋ C))) → (B ⊆ (B ∨ℋ C) ∧ x ⊆ (B ∨ℋ C)))
55		chlubt 5426	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((B ∈ Cℋ ∧ x ∈ Cℋ ∧ (B ∨ℋ C) ∈ Cℋ ) → ((B ⊆ (B ∨ℋ C) ∧ x ⊆ (B ∨ℋ C)) ↔ (B ∨ℋ x) ⊆ (B ∨ℋ C)))
56		3simp2 595	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((B ∈ Cℋ ∧ x ∈ Cℋ ∧ C ∈ Cℋ ) → x ∈ Cℋ )
57		chjclt 5330	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((B ∈ Cℋ ∧ C ∈ Cℋ ) → (B ∨ℋ C) ∈ Cℋ )
58	57	3adant2 598	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((B ∈ Cℋ ∧ x ∈ Cℋ ∧ C ∈ Cℋ ) → (B ∨ℋ C) ∈ Cℋ )
59	55, 41, 56, 58	syl3anc 629	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((B ∈ Cℋ ∧ x ∈ Cℋ ∧ C ∈ Cℋ ) → ((B ⊆ (B ∨ℋ C) ∧ x ⊆ (B ∨ℋ C)) ↔ (B ∨ℋ x) ⊆ (B ∨ℋ C)))
60	59	adantr 306	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((B ∈ Cℋ ∧ x ∈ Cℋ ∧ C ∈ Cℋ ) ∧ ((x ⊆ A ∧ ¬ B ⊆ A) ∧ A ⊂ (B ∨ℋ C))) → ((B ⊆ (B ∨ℋ C) ∧ x ⊆ (B ∨ℋ C)) ↔ (B ∨ℋ x) ⊆ (B ∨ℋ C)))
61	54, 60	mpbid 170	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((B ∈ Cℋ ∧ x ∈ Cℋ ∧ C ∈ Cℋ ) ∧ ((x ⊆ A ∧ ¬ B ⊆ A) ∧ A ⊂ (B ∨ℋ C))) → (B ∨ℋ x) ⊆ (B ∨ℋ C))
62	10, 14, 46	im3an 605	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) → (B ∈ Cℋ ∧ x ∈ Cℋ ∧ C ∈ Cℋ ))
63	61, 62	sylan 343	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ ((x ⊆ A ∧ ¬ B ⊆ A) ∧ A ⊂ (B ∨ℋ C))) → (B ∨ℋ x) ⊆ (B ∨ℋ C))
64	51, 63	eqssd 1518	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ ((x ⊆ A ∧ ¬ B ⊆ A) ∧ A ⊂ (B ∨ℋ C))) → (B ∨ℋ C) = (B ∨ℋ x))
65	64	anassrs 338	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ (x ⊆ A ∧ ¬ B ⊆ A)) ∧ A ⊂ (B ∨ℋ C)) → (B ∨ℋ C) = (B ∨ℋ x))
66	65	psseq2d 1565	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ (x ⊆ A ∧ ¬ B ⊆ A)) ∧ A ⊂ (B ∨ℋ C)) → (A ⊂ (B ∨ℋ C) ↔ A ⊂ (B ∨ℋ x)))
67	66	exp 291	. . . . . . . . . . . . . . . . . 18 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ (x ⊆ A ∧ ¬ B ⊆ A)) → (A ⊂ (B ∨ℋ C) → (A ⊂ (B ∨ℋ C) ↔ A ⊂ (B ∨ℋ x))))
68	67	ibd 451	. . . . . . . . . . . . . . . . 17 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) ∧ (x ⊆ A ∧ ¬ B ⊆ A)) → (A ⊂ (B ∨ℋ C) → A ⊂ (B ∨ℋ x)))
69	68	exp32 294	. . . . . . . . . . . . . . . 16 ⊢ ((B ∈ Atoms ∧ x ∈ Atoms ∧ C ∈ Atoms) → (x ⊆ A → (¬ B ⊆ A → (A ⊂ (B ∨ℋ C) → A ⊂ (B ∨ℋ x)))))
70	69	3expa 612	. . . . . . . . . . . . . . 15 ⊢ (((B ∈ Atoms ∧ x ∈ Atoms) ∧ C ∈ Atoms) → (x ⊆ A → (¬ B ⊆ A → (A ⊂ (B ∨ℋ C) → A ⊂ (B ∨ℋ x)))))
71	70	an1rs 373	. . . . . . . . . . . . . 14 ⊢ (((B ∈ Atoms ∧ C ∈ Atoms) ∧ x ∈ Atoms) → (x ⊆ A → (¬ B ⊆ A → (A ⊂ (B ∨ℋ C) → A ⊂ (B ∨ℋ x)))))
72	71	com34 36	. . . . . . . . . . . . 13 ⊢ (((B ∈ Atoms ∧ C ∈ Atoms) ∧ x ∈ Atoms) → (x ⊆ A → (A ⊂ (B ∨ℋ C) → (¬ B ⊆ A → A ⊂ (B ∨ℋ x)))))
73	72	imp45 290	. . . . . . . . . . . 12 ⊢ ((((B ∈ Atoms ∧ C ∈ Atoms) ∧ x ∈ Atoms) ∧ (x ⊆ A ∧ (A ⊂ (B ∨ℋ C) ∧ ¬ B ⊆ A))) → A ⊂ (B ∨ℋ x))
74		pm3.27 260	. . . . . . . . . . . . . . . . . 18 ⊢ ((B ∈ Cℋ ∧ x ∈ Cℋ ) → x ∈ Cℋ )
75	74, 43	jca 236	. . . . . . . . . . . . . . . . 17 ⊢ ((B ∈ Cℋ ∧ x ∈ Cℋ<SUB> ) → (x ∈ Cℋ ∧ (B ∨ℋ x) ∈ Cℋ ))
75, 10, 14	syl2an 349	. . . . . . . . . . . . . . . 16 ⊢ ((B ∈ Atoms ∧ x ∈ Atoms) → (x ∈ Cℋ ∧ (B ∨ℋ x) ∈ Cℋ ))
77		atoml.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ A ∈ Cℋ
78		cvnbtwn3t 5720	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((x ∈ Cℋ ∧ (B ∨ℋ x) ∈ Cℋ ∧ A ∈ Cℋ ) → (x ⋖ (B ∨ℋ x) → ((x ⊆ A ∧ A ⊂ (B ∨ℋ x)) → A = x)))
79	77, 78	mp3an3 641	. . . . . . . . . . . . . . . . . . 19 ⊢ ((x ∈ Cℋ ∧ (B ∨ℋ x) ∈ Cℋ ) → (x ⋖ (B ∨ℋ x) → ((x ⊆ A ∧ A ⊂ (B ∨ℋ x)) → A = x)))
80	79	exp4a 295	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∈ Cℋ ∧ (B ∨ℋ x) ∈ Cℋ ) → (x ⋖ (B ∨ℋ x) → (x ⊆ A → (A ⊂ (B ∨ℋ x) → A = x))))
81	80	com23 32	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ Cℋ ∧ (B ∨ℋ x) ∈ Cℋ ) → (x ⊆ A → (x ⋖ (B ∨ℋ x) → (A ⊂ (B ∨ℋ x) → A = x))))
82	81	imp4a 282	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ Cℋ ∧ (B ∨ℋ x) ∈ Cℋ ) → (x ⊆ A → ((x ⋖ (B ∨ℋ x) ∧ A ⊂ (B ∨ℋ x)) → A = x)))
83	76, 82	syl 12	. . . . . . . . . . . . . . 15 ⊢ ((B ∈ Atoms ∧ x ∈ Atoms) → (x ⊆ A → ((x ⋖ (B ∨ℋ x) ∧ A ⊂ (B ∨ℋ x)) → A = x)))
84	83	adantlr 310	. . . . . . . . . . . . . 14 ⊢ (((B ∈ Atoms ∧ C ∈ Atoms) ∧ x ∈ Atoms) → (x ⊆ A → ((x ⋖ (B ∨ℋ x) ∧ A ⊂ (B ∨ℋ x)) → A = x)))
85	84	imp 277	. . . . . . . . . . . . 13 ⊢ ((((B ∈ Atoms ∧ C ∈ Atoms) ∧ x ∈ Atoms) ∧ x ⊆ A) → ((x ⋖ (B ∨ℋ x) ∧ A ⊂ (B ∨ℋ x)) → A = x))
86	85	adantrr 312	. . . . . . . . . . . 12 ⊢ ((((B ∈ Atoms ∧ C ∈ Atoms) ∧ x ∈ Atoms) ∧ (x ⊆ A ∧ (A ⊂ (B ∨ℋ C) ∧ ¬ B ⊆ A))) → ((x ⋖ (B ∨ℋ x) ∧ A ⊂ (B ∨ℋ x)) → A = x))
87	19, 73, 86	mp2and 526	. . . . . . . . . . 11 ⊢ ((((B ∈ Atoms ∧ C ∈ Atoms) ∧ x ∈ Atoms) ∧ (x ⊆ A ∧ (A ⊂ (B ∨ℋ C) ∧ ¬ B ⊆ A))) → A = x)
88	87	eleq1d 1155	. . . . . . . . . 10 ⊢ ((((B ∈ Atoms ∧ C ∈ Atoms) ∧ x ∈ Atoms) ∧ (x ⊆ A ∧ (A ⊂ (B ∨ℋ C) ∧ ¬ B ⊆ A))) → (A ∈ Atoms ↔ x ∈ Atoms))
89	88	biimprcd 138	. . . . . . . . 9 ⊢ (x ∈ Atoms → ((((B ∈ Atoms ∧ C ∈ Atoms) ∧ x ∈ Atoms) ∧ (x ⊆ A ∧ (A ⊂ (B ∨ℋ C) ∧ ¬ B ⊆ A))) → A ∈ Atoms))
90	89	exp4c 297	. . . . . . . 8 ⊢ (x ∈ Atoms → ((B ∈ Atoms ∧ C ∈ Atoms) → (x ∈ Atoms → ((x ⊆ A ∧ (A ⊂ (B ∨ℋ C) ∧ ¬ B ⊆ A)) → A ∈ Atoms))))
91	90	pm2.43b 61	. . . . . . 7 ⊢ ((B ∈ Atoms ∧ C ∈ Atoms) → (x ∈ Atoms → ((x ⊆ A ∧ (A ⊂ (B ∨ℋ C) ∧ ¬ B ⊆ A)) → A ∈ Atoms)))
92	91	imp 277	. . . . . 6 ⊢ (((B ∈ Atoms ∧ C ∈ Atoms) ∧ x ∈ Atoms) → ((x ⊆ A ∧ (A ⊂ (B ∨ℋ C) ∧ ¬ B ⊆ A)) → A ∈ Atoms))
93	92	exp4d 298	. . . . 5 ⊢ (((B ∈ Atoms ∧ C ∈ Atoms) ∧ x ∈ Atoms) → (x ⊆ A → (A ⊂ (B ∨ℋ C) → (¬ B ⊆ A → A ∈ Atoms))))
94	93	exp 291	. . . 4 ⊢ ((B ∈ Atoms ∧ C ∈ Atoms) → (x ∈ Atoms → (x ⊆ A → (A ⊂ (B ∨ℋ C) → (¬ B ⊆ A → A ∈ Atoms)))))
95	94	r19.23adv 1286	. . 3 ⊢ ((B ∈ Atoms ∧ C ∈ Atoms) → (∃x ∈ Atoms x ⊆ A → (A ⊂ (B ∨ℋ C) → (¬ B ⊆ A → A ∈ Atoms))))
96	77	hatomic 5754	. . 3 ⊢ (¬ A = 0ℋ → ∃x ∈ Atoms x ⊆ A)
97	95, 96	syl5 22	. 2 ⊢ ((B ∈ Atoms ∧ C ∈ Atoms) → (¬ A = 0ℋ → (A ⊂ (B ∨ℋ C) → (¬ B ⊆ A → A ∈ Atoms))))
98	97	imp32 281	1 ⊢ (((B ∈ Atoms ∧ C ∈ Atoms) ∧ (¬ A = 0ℋ ∧ A ⊂ (B ∨ℋ C))) → (¬ B ⊆ A → A ∈ Atoms))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196   ∧ w3a 581   = wceq 1091   ∈ wcel 1092  ∃wrex 1202   ∩ cin 1486   ⊆ wss 1487   ⊂ wpss 1488   class class class wbr 2054  (class class class)co 3001   C_ℋ cch 4968   ∨_ℋ chj 4972  0_ℋc0h 4974  Atomscat 4980   ⋖ ccv 4981

This theorem is referenced by:  atcvat 5771

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079  ax-ac 1080  ax-hilex 4983  ax-hvaddcl 4984  ax-hvcom 4985  ax-hvass 4986  ax-hvzercl 4987  ax-hvaddid 4988  ax-hvmulcl 4989  ax-hvmulid 4991  ax-hvmulass 4992  ax-hvdistr1 4993  ax-hvdistr2 4994  ax-hvmulzer 4995  ax-hicl 5043  ax-his1 5045  ax-his2 5046  ax-his3 5047  ax-his4 5048  ax-hcompl 5113

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-sup 2154  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-rdg 2970  df-opr 3003  df-oprab 3004  df-1st 3087  df-2nd 3088  df-1o 3104  df-oadd 3106  df-omul 3107  df-er 3200  df-ec 3202  df-qs 3205  df-ni 3794  df-pli 3795  df-mi 3796  df-lti 3797  df-plpq 3829  df-mpq 3830  df-enq 3831  df-nq 3832  df-plq 3833  df-mq 3834  df-rq 3835  df-ltq 3836  df-1q 3837  df-np 3880  df-1p 3881  df-plp 3882  df-mp 3883  df-ltp 3884  df-plpr 3958  df-mpr 3959  df-enr 3960  df-nr 3961  df-plr 3962  df-mr 3963  df-ltr 3964  df-0r 3965  df-1r 3966  df-m1r 3967  df-c 4034  df-0 4035  df-1 4036  df-i 4037  df-r 4038  df-plus 4039  df-mul 4040  df-lt 4041  df-sub 4133  df-neg 4135  df-div 4216  df-le 4277  df-n 4423  df-2 4462  df-3 4463  df-4 4464  df-n0 4535  df-z 4564  df-seq 4661  df-exp 4676  df-sqr 4728  df-re 4790  df-im 4791  df-cj 4792  df-abs 4793  df-clim 4876  df-hvsub 4996  df-hnorm 5074  df-cauchy 5102  df-hlim 5107  df-sh 5114  df-ch 5127  df-oc 5156  df-ch0 5157  df-pj 5244  df-shsum 5275  df-span 5276  df-chj 5277  df-chsup 5278  df-cv 5712  df-at 5737

metamath.org