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 ⊢ A ∈ V
dfon2lem5.2 ⊢ B ∈ V
Assertion dfon2lem5 ⊢ ∀ x x ⊂ A ∧ Tr ⁡ x → x ∈ A ∧ ∀ y y ⊂ B ∧ Tr ⁡ y → y ∈ B → A ∈ B ∨ A = B ∨ B ∈ A

Proof

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