Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dfon2lem8 Structured version   Visualization version   GIF version

Theorem dfon2lem8 35322
Description: Lemma for dfon2 35324. The intersection of a nonempty class 𝐴 of new ordinals is itself a new ordinal and is contained within 𝐴 (Contributed by Scott Fenton, 26-Feb-2011.)
Assertion
Ref Expression
dfon2lem8 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) ∧ 𝐴𝐴))
Distinct variable group:   𝑥,𝐴,𝑦,𝑧

Proof of Theorem dfon2lem8
Dummy variables 𝑤 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3473 . . . . . . 7 𝑥 ∈ V
2 dfon2lem3 35317 . . . . . . 7 (𝑥 ∈ V → (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (Tr 𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧𝑧)))
31, 2ax-mp 5 . . . . . 6 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (Tr 𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧𝑧))
43simpld 494 . . . . 5 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → Tr 𝑥)
54ralimi 3078 . . . 4 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑥𝐴 Tr 𝑥)
6 trint 5277 . . . 4 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
75, 6syl 17 . . 3 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → Tr 𝐴)
87adantl 481 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → Tr 𝐴)
91dfon2lem7 35321 . . . . . . 7 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
109alrimiv 1923 . . . . . 6 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
1110ralimi 3078 . . . . 5 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑥𝐴𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
12 df-ral 3057 . . . . . . 7 (∀𝑥𝐴𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑥(𝑥𝐴 → ∀𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
13 19.21v 1935 . . . . . . . 8 (∀𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))) ↔ (𝑥𝐴 → ∀𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
1413albii 1814 . . . . . . 7 (∀𝑥𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))) ↔ ∀𝑥(𝑥𝐴 → ∀𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
1512, 14bitr4i 278 . . . . . 6 (∀𝑥𝐴𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑥𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
16 impexp 450 . . . . . . . 8 (((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ (𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
17162albii 1815 . . . . . . 7 (∀𝑥𝑤((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑥𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
18 eluni2 4907 . . . . . . . . . . 11 (𝑤 𝐴 ↔ ∃𝑥𝐴 𝑤𝑥)
1918biimpi 215 . . . . . . . . . 10 (𝑤 𝐴 → ∃𝑥𝐴 𝑤𝑥)
2019imim1i 63 . . . . . . . . 9 ((∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → (𝑤 𝐴 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
2120alimi 1806 . . . . . . . 8 (∀𝑤(∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → ∀𝑤(𝑤 𝐴 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
22 alcom 2149 . . . . . . . . 9 (∀𝑥𝑤((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑤𝑥((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
23 19.23v 1938 . . . . . . . . . . 11 (∀𝑥((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ (∃𝑥(𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
24 df-rex 3066 . . . . . . . . . . . 12 (∃𝑥𝐴 𝑤𝑥 ↔ ∃𝑥(𝑥𝐴𝑤𝑥))
2524imbi1i 349 . . . . . . . . . . 11 ((∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ (∃𝑥(𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
2623, 25bitr4i 278 . . . . . . . . . 10 (∀𝑥((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ (∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
2726albii 1814 . . . . . . . . 9 (∀𝑤𝑥((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑤(∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
2822, 27bitri 275 . . . . . . . 8 (∀𝑥𝑤((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑤(∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
29 df-ral 3057 . . . . . . . 8 (∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤) ↔ ∀𝑤(𝑤 𝐴 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
3021, 28, 293imtr4i 292 . . . . . . 7 (∀𝑥𝑤((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
3117, 30sylbir 234 . . . . . 6 (∀𝑥𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
3215, 31sylbi 216 . . . . 5 (∀𝑥𝐴𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
3311, 32syl 17 . . . 4 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
3433adantl 481 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
35 intssuni 4968 . . . . 5 (𝐴 ≠ ∅ → 𝐴 𝐴)
36 ssralv 4046 . . . . 5 ( 𝐴 𝐴 → (∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
3735, 36syl 17 . . . 4 (𝐴 ≠ ∅ → (∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
3837adantr 480 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
3934, 38mpd 15 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
40 dfon2lem6 35320 . . 3 ((Tr 𝐴 ∧ ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴))
41 intex 5333 . . . . . . . . . . 11 (𝐴 ≠ ∅ ↔ 𝐴 ∈ V)
42 dfon2lem3 35317 . . . . . . . . . . 11 ( 𝐴 ∈ V → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) → (Tr 𝐴 ∧ ∀𝑡 𝐴 ¬ 𝑡𝑡)))
4341, 42sylbi 216 . . . . . . . . . 10 (𝐴 ≠ ∅ → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) → (Tr 𝐴 ∧ ∀𝑡 𝐴 ¬ 𝑡𝑡)))
4443imp 406 . . . . . . . . 9 ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (Tr 𝐴 ∧ ∀𝑡 𝐴 ¬ 𝑡𝑡))
4544simprd 495 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ∀𝑡 𝐴 ¬ 𝑡𝑡)
46 untelirr 35238 . . . . . . . 8 (∀𝑡 𝐴 ¬ 𝑡𝑡 → ¬ 𝐴 𝐴)
4745, 46syl 17 . . . . . . 7 ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ¬ 𝐴 𝐴)
4847adantlr 714 . . . . . 6 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ¬ 𝐴 𝐴)
49 risset 3225 . . . . . . . . . 10 ( 𝐴𝐴 ↔ ∃𝑡𝐴 𝑡 = 𝐴)
5049notbii 320 . . . . . . . . 9 𝐴𝐴 ↔ ¬ ∃𝑡𝐴 𝑡 = 𝐴)
51 ralnex 3067 . . . . . . . . 9 (∀𝑡𝐴 ¬ 𝑡 = 𝐴 ↔ ¬ ∃𝑡𝐴 𝑡 = 𝐴)
5250, 51bitr4i 278 . . . . . . . 8 𝐴𝐴 ↔ ∀𝑡𝐴 ¬ 𝑡 = 𝐴)
53 eqcom 2734 . . . . . . . . . . . 12 (𝑡 = 𝐴 𝐴 = 𝑡)
5453notbii 320 . . . . . . . . . . 11 𝑡 = 𝐴 ↔ ¬ 𝐴 = 𝑡)
5544simpld 494 . . . . . . . . . . . . 13 ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → Tr 𝐴)
5655adantlr 714 . . . . . . . . . . . 12 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → Tr 𝐴)
57 psseq2 4084 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑡 → (𝑦𝑥𝑦𝑡))
5857anbi1d 629 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑡 → ((𝑦𝑥 ∧ Tr 𝑦) ↔ (𝑦𝑡 ∧ Tr 𝑦)))
59 elequ2 2114 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑡 → (𝑦𝑥𝑦𝑡))
6058, 59imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑡 → (((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) ↔ ((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
6160albidv 1916 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑡 → (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) ↔ ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
6261rspccv 3604 . . . . . . . . . . . . . . 15 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (𝑡𝐴 → ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
6362adantl 481 . . . . . . . . . . . . . 14 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (𝑡𝐴 → ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
64 intss1 4961 . . . . . . . . . . . . . . . 16 (𝑡𝐴 𝐴𝑡)
65 dfpss2 4081 . . . . . . . . . . . . . . . . . . . 20 ( 𝐴𝑡 ↔ ( 𝐴𝑡 ∧ ¬ 𝐴 = 𝑡))
66 psseq1 4083 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝐴 → (𝑦𝑡 𝐴𝑡))
67 treq 5267 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝐴 → (Tr 𝑦 ↔ Tr 𝐴))
6866, 67anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝐴 → ((𝑦𝑡 ∧ Tr 𝑦) ↔ ( 𝐴𝑡 ∧ Tr 𝐴)))
69 eleq1 2816 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝐴 → (𝑦𝑡 𝐴𝑡))
7068, 69imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝐴 → (((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ (( 𝐴𝑡 ∧ Tr 𝐴) → 𝐴𝑡)))
7170spcgv 3581 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝐴 ∈ V → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (( 𝐴𝑡 ∧ Tr 𝐴) → 𝐴𝑡)))
7241, 71sylbi 216 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ≠ ∅ → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (( 𝐴𝑡 ∧ Tr 𝐴) → 𝐴𝑡)))
7372imp 406 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (( 𝐴𝑡 ∧ Tr 𝐴) → 𝐴𝑡))
7473expd 415 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → ( 𝐴𝑡 → (Tr 𝐴 𝐴𝑡)))
7565, 74biimtrrid 242 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (( 𝐴𝑡 ∧ ¬ 𝐴 = 𝑡) → (Tr 𝐴 𝐴𝑡)))
7675exp4b 430 . . . . . . . . . . . . . . . . . 18 (𝐴 ≠ ∅ → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ( 𝐴𝑡 → (¬ 𝐴 = 𝑡 → (Tr 𝐴 𝐴𝑡)))))
7776com45 97 . . . . . . . . . . . . . . . . 17 (𝐴 ≠ ∅ → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ( 𝐴𝑡 → (Tr 𝐴 → (¬ 𝐴 = 𝑡 𝐴𝑡)))))
7877com23 86 . . . . . . . . . . . . . . . 16 (𝐴 ≠ ∅ → ( 𝐴𝑡 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝐴 → (¬ 𝐴 = 𝑡 𝐴𝑡)))))
7964, 78syl5 34 . . . . . . . . . . . . . . 15 (𝐴 ≠ ∅ → (𝑡𝐴 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝐴 → (¬ 𝐴 = 𝑡 𝐴𝑡)))))
8079adantr 480 . . . . . . . . . . . . . 14 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (𝑡𝐴 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝐴 → (¬ 𝐴 = 𝑡 𝐴𝑡)))))
8163, 80mpdd 43 . . . . . . . . . . . . 13 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (𝑡𝐴 → (Tr 𝐴 → (¬ 𝐴 = 𝑡 𝐴𝑡))))
8281adantr 480 . . . . . . . . . . . 12 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (𝑡𝐴 → (Tr 𝐴 → (¬ 𝐴 = 𝑡 𝐴𝑡))))
8356, 82mpid 44 . . . . . . . . . . 11 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (𝑡𝐴 → (¬ 𝐴 = 𝑡 𝐴𝑡)))
8454, 83syl7bi 255 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (𝑡𝐴 → (¬ 𝑡 = 𝐴 𝐴𝑡)))
8584ralrimiv 3140 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ∀𝑡𝐴𝑡 = 𝐴 𝐴𝑡))
86 ralim 3081 . . . . . . . . 9 (∀𝑡𝐴𝑡 = 𝐴 𝐴𝑡) → (∀𝑡𝐴 ¬ 𝑡 = 𝐴 → ∀𝑡𝐴 𝐴𝑡))
8785, 86syl 17 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (∀𝑡𝐴 ¬ 𝑡 = 𝐴 → ∀𝑡𝐴 𝐴𝑡))
8852, 87biimtrid 241 . . . . . . 7 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (¬ 𝐴𝐴 → ∀𝑡𝐴 𝐴𝑡))
89 elintg 4952 . . . . . . . . 9 ( 𝐴 ∈ V → ( 𝐴 𝐴 ↔ ∀𝑡𝐴 𝐴𝑡))
9041, 89sylbi 216 . . . . . . . 8 (𝐴 ≠ ∅ → ( 𝐴 𝐴 ↔ ∀𝑡𝐴 𝐴𝑡))
9190ad2antrr 725 . . . . . . 7 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ( 𝐴 𝐴 ↔ ∀𝑡𝐴 𝐴𝑡))
9288, 91sylibrd 259 . . . . . 6 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (¬ 𝐴𝐴 𝐴 𝐴))
9348, 92mt3d 148 . . . . 5 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → 𝐴𝐴)
9493ex 412 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) → 𝐴𝐴))
9594ancld 550 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) ∧ 𝐴𝐴)))
9640, 95syl5 34 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → ((Tr 𝐴 ∧ ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) ∧ 𝐴𝐴)))
978, 39, 96mp2and 698 1 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) ∧ 𝐴𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wal 1532   = wceq 1534  wex 1774  wcel 2099  wne 2935  wral 3056  wrex 3065  Vcvv 3469  wss 3944  wpss 3945  c0 4318   cuni 4903   cint 4944  Tr wtr 5259
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-pw 4600  df-sn 4625  df-pr 4627  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-tr 5260  df-suc 6369
This theorem is referenced by:  dfon2lem9  35323
  Copyright terms: Public domain W3C validator