Theorem chrelat2i

Description: A consequence of relative atomicity. (Contributed by NM, 30-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	chpssat.1	⊢ 𝐴 ∈ Cℋ
	chpssat.2	⊢ 𝐵 ∈ Cℋ
Assertion	chrelat2i	⊢ ( ¬ 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		chpssat.1	⊢ 𝐴 ∈ Cℋ
2		chpssat.2	⊢ 𝐵 ∈ Cℋ
3		nssinpss	⊢ ( ¬ 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 )
4	1 2	chincli	⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
5	4 1	chrelati	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 → ∃ 𝑥 ∈ HAtoms ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐴 ) )
6		atelch	⊢ ( 𝑥 ∈ HAtoms → 𝑥 ∈ Cℋ )
7		chlub	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐴 ) )
8	4 1 7	mp3an13	⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐴 ) )
9		simpr	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 ⊆ 𝐴 )
10	8 9	syl6bir	⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐴 → 𝑥 ⊆ 𝐴 ) )
11	10	adantld	⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐴 ) → 𝑥 ⊆ 𝐴 ) )
12		ssin	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )
13	12	notbii	⊢ ( ¬ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )
14		chnle	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) )
15	4 14	mpan	⊢ ( 𝑥 ∈ Cℋ → ( ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) )
16	13 15	syl5bb	⊢ ( 𝑥 ∈ Cℋ → ( ¬ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) )
17	16 8	anbi12d	⊢ ( 𝑥 ∈ Cℋ → ( ( ¬ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴 ) ) ↔ ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐴 ) ) )
18		pm3.21	⊢ ( 𝑥 ⊆ 𝐵 → ( 𝑥 ⊆ 𝐴 → ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) )
19		orcom	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ∨ ¬ 𝑥 ⊆ 𝐴 ) ↔ ( ¬ 𝑥 ⊆ 𝐴 ∨ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) )
20		pm4.55	⊢ ( ¬ ( ¬ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑥 ⊆ 𝐴 ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ∨ ¬ 𝑥 ⊆ 𝐴 ) )
21		imor	⊢ ( ( 𝑥 ⊆ 𝐴 → ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) ↔ ( ¬ 𝑥 ⊆ 𝐴 ∨ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) )
22	19 20 21	3bitr4ri	⊢ ( ( 𝑥 ⊆ 𝐴 → ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) ↔ ¬ ( ¬ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑥 ⊆ 𝐴 ) )
23	18 22	sylib	⊢ ( 𝑥 ⊆ 𝐵 → ¬ ( ¬ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑥 ⊆ 𝐴 ) )
24	23	con2i	⊢ ( ( ¬ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑥 ⊆ 𝐴 ) → ¬ 𝑥 ⊆ 𝐵 )
25	24	adantrl	⊢ ( ( ¬ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴 ) ) → ¬ 𝑥 ⊆ 𝐵 )
26	17 25	syl6bir	⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐴 ) → ¬ 𝑥 ⊆ 𝐵 ) )
27	11 26	jcad	⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐴 ) → ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) ) )
28	6 27	syl	⊢ ( 𝑥 ∈ HAtoms → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐴 ) → ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) ) )
29	28	reximia	⊢ ( ∃ 𝑥 ∈ HAtoms ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐴 ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) )
30	5 29	syl	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) )
31	3 30	sylbi	⊢ ( ¬ 𝐴 ⊆ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) )
32		sstr2	⊢ ( 𝑥 ⊆ 𝐴 → ( 𝐴 ⊆ 𝐵 → 𝑥 ⊆ 𝐵 ) )
33	32	com12	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) )
34	33	ralrimivw	⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) )
35		iman	⊢ ( ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) ↔ ¬ ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) )
36	35	ralbii	⊢ ( ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) ↔ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) )
37		ralnex	⊢ ( ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) ↔ ¬ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) )
38	36 37	bitri	⊢ ( ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) ↔ ¬ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) )
39	34 38	sylib	⊢ ( 𝐴 ⊆ 𝐵 → ¬ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) )
40	39	con2i	⊢ ( ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) → ¬ 𝐴 ⊆ 𝐵 )
41	31 40	impbii	⊢ ( ¬ 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) )