Metamath Proof Explorer

Theorem dfon2lem5

Description: Lemma for dfon2 . Two sets satisfying the new definition also satisfy trichotomy with respect to e. . (Contributed by Scott Fenton, 25-Feb-2011)

Ref Expression
Hypotheses dfon2lem5.1 ⊢ 𝐴 ∈ V
dfon2lem5.2 ⊢ 𝐵 ∈ V
Assertion dfon2lem5 ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 dfon2lem5.1 ⊢ 𝐴 ∈ V
2 dfon2lem5.2 ⊢ 𝐵 ∈ V
3 1 2 dfon2lem4 ⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )
4 dfpss2 ⊢ ( 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵 ) )
5 dfpss2 ⊢ ( 𝐵 ⊊ 𝐴 ↔ ( 𝐵 ⊆ 𝐴 ∧ ¬ 𝐵 = 𝐴 ) )
6 eqcom ⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 )
7 6 notbii ⊢ ( ¬ 𝐵 = 𝐴 ↔ ¬ 𝐴 = 𝐵 )
8 7 anbi2i ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ ¬ 𝐵 = 𝐴 ) ↔ ( 𝐵 ⊆ 𝐴 ∧ ¬ 𝐴 = 𝐵 ) )
9 5 8 bitri ⊢ ( 𝐵 ⊊ 𝐴 ↔ ( 𝐵 ⊆ 𝐴 ∧ ¬ 𝐴 = 𝐵 ) )
10 4 9 orbi12i ⊢ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐵 ⊊ 𝐴 ) ↔ ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵 ) ∨ ( 𝐵 ⊆ 𝐴 ∧ ¬ 𝐴 = 𝐵 ) ) )
11 andir ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ∧ ¬ 𝐴 = 𝐵 ) ↔ ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵 ) ∨ ( 𝐵 ⊆ 𝐴 ∧ ¬ 𝐴 = 𝐵 ) ) )
12 10 11 bitr4i ⊢ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐵 ⊊ 𝐴 ) ↔ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ∧ ¬ 𝐴 = 𝐵 ) )
13 orcom ⊢ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐵 ⊊ 𝐴 ) ↔ ( 𝐵 ⊊ 𝐴 ∨ 𝐴 ⊊ 𝐵 ) )
14 dfon2lem3 ⊢ ( 𝐵 ∈ V → ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) → ( Tr 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 ∈ 𝑧 ) ) )
15 2 14 ax-mp ⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) → ( Tr 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 ∈ 𝑧 ) )
16 15 simpld ⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) → Tr 𝐵 )
17 psseq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ⊊ 𝐴 ↔ 𝐵 ⊊ 𝐴 ) )
18 treq ⊢ ( 𝑥 = 𝐵 → ( Tr 𝑥 ↔ Tr 𝐵 ) )
19 17 18 anbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) ↔ ( 𝐵 ⊊ 𝐴 ∧ Tr 𝐵 ) ) )
20 eleq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
21 19 20 imbi12d ⊢ ( 𝑥 = 𝐵 → ( ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ↔ ( ( 𝐵 ⊊ 𝐴 ∧ Tr 𝐵 ) → 𝐵 ∈ 𝐴 ) ) )
22 2 21 spcv ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( ( 𝐵 ⊊ 𝐴 ∧ Tr 𝐵 ) → 𝐵 ∈ 𝐴 ) )
23 22 expcomd ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( Tr 𝐵 → ( 𝐵 ⊊ 𝐴 → 𝐵 ∈ 𝐴 ) ) )
24 23 imp ⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ Tr 𝐵 ) → ( 𝐵 ⊊ 𝐴 → 𝐵 ∈ 𝐴 ) )
25 16 24 sylan2 ⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( 𝐵 ⊊ 𝐴 → 𝐵 ∈ 𝐴 ) )
26 dfon2lem3 ⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( Tr 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧 ) ) )
27 1 26 ax-mp ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( Tr 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧 ) )
28 27 simpld ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → Tr 𝐴 )
29 psseq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ⊊ 𝐵 ↔ 𝐴 ⊊ 𝐵 ) )
30 treq ⊢ ( 𝑦 = 𝐴 → ( Tr 𝑦 ↔ Tr 𝐴 ) )
31 29 30 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) ↔ ( 𝐴 ⊊ 𝐵 ∧ Tr 𝐴 ) ) )
32 eleq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
33 31 32 imbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ↔ ( ( 𝐴 ⊊ 𝐵 ∧ Tr 𝐴 ) → 𝐴 ∈ 𝐵 ) ) )
34 1 33 spcv ⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) → ( ( 𝐴 ⊊ 𝐵 ∧ Tr 𝐴 ) → 𝐴 ∈ 𝐵 ) )
35 34 expcomd ⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) → ( Tr 𝐴 → ( 𝐴 ⊊ 𝐵 → 𝐴 ∈ 𝐵 ) ) )
36 28 35 mpan9 ⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( 𝐴 ⊊ 𝐵 → 𝐴 ∈ 𝐵 ) )
37 25 36 orim12d ⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( ( 𝐵 ⊊ 𝐴 ∨ 𝐴 ⊊ 𝐵 ) → ( 𝐵 ∈ 𝐴 ∨ 𝐴 ∈ 𝐵 ) ) )
38 13 37 syl5bi ⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( ( 𝐴 ⊊ 𝐵 ∨ 𝐵 ⊊ 𝐴 ) → ( 𝐵 ∈ 𝐴 ∨ 𝐴 ∈ 𝐵 ) ) )
39 12 38 syl5bir ⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ∧ ¬ 𝐴 = 𝐵 ) → ( 𝐵 ∈ 𝐴 ∨ 𝐴 ∈ 𝐵 ) ) )
40 3 39 mpand ⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( ¬ 𝐴 = 𝐵 → ( 𝐵 ∈ 𝐴 ∨ 𝐴 ∈ 𝐵 ) ) )
41 3orrot ⊢ ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ∨ 𝐴 ∈ 𝐵 ) )
42 3orass ⊢ ( ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ∨ 𝐴 ∈ 𝐵 ) ↔ ( 𝐴 = 𝐵 ∨ ( 𝐵 ∈ 𝐴 ∨ 𝐴 ∈ 𝐵 ) ) )
43 df-or ⊢ ( ( 𝐴 = 𝐵 ∨ ( 𝐵 ∈ 𝐴 ∨ 𝐴 ∈ 𝐵 ) ) ↔ ( ¬ 𝐴 = 𝐵 → ( 𝐵 ∈ 𝐴 ∨ 𝐴 ∈ 𝐵 ) ) )
44 42 43 bitri ⊢ ( ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ∨ 𝐴 ∈ 𝐵 ) ↔ ( ¬ 𝐴 = 𝐵 → ( 𝐵 ∈ 𝐴 ∨ 𝐴 ∈ 𝐵 ) ) )
45 41 44 bitri ⊢ ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ↔ ( ¬ 𝐴 = 𝐵 → ( 𝐵 ∈ 𝐴 ∨ 𝐴 ∈ 𝐵 ) ) )
46 40 45 sylibr ⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) )