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 34365
Description: Lemma for dfon2 34367. 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 3449 . . . . . . 7 𝑥 ∈ V
2 dfon2lem3 34360 . . . . . . 7 (𝑥 ∈ V → (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (Tr 𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧𝑧)))
31, 2ax-mp 5 . . . . . 6 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (Tr 𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧𝑧))
43simpld 495 . . . . 5 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → Tr 𝑥)
54ralimi 3086 . . . 4 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑥𝐴 Tr 𝑥)
6 trint 5240 . . . 4 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
75, 6syl 17 . . 3 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → Tr 𝐴)
87adantl 482 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → Tr 𝐴)
91dfon2lem7 34364 . . . . . . 7 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
109alrimiv 1930 . . . . . 6 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
1110ralimi 3086 . . . . 5 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑥𝐴𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
12 df-ral 3065 . . . . . . 7 (∀𝑥𝐴𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑥(𝑥𝐴 → ∀𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
13 19.21v 1942 . . . . . . . 8 (∀𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))) ↔ (𝑥𝐴 → ∀𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
1413albii 1821 . . . . . . 7 (∀𝑥𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))) ↔ ∀𝑥(𝑥𝐴 → ∀𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
1512, 14bitr4i 277 . . . . . 6 (∀𝑥𝐴𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑥𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
16 impexp 451 . . . . . . . 8 (((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ (𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
17162albii 1822 . . . . . . 7 (∀𝑥𝑤((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑥𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
18 eluni2 4869 . . . . . . . . . . 11 (𝑤 𝐴 ↔ ∃𝑥𝐴 𝑤𝑥)
1918biimpi 215 . . . . . . . . . 10 (𝑤 𝐴 → ∃𝑥𝐴 𝑤𝑥)
2019imim1i 63 . . . . . . . . 9 ((∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → (𝑤 𝐴 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
2120alimi 1813 . . . . . . . 8 (∀𝑤(∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → ∀𝑤(𝑤 𝐴 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
22 alcom 2156 . . . . . . . . 9 (∀𝑥𝑤((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑤𝑥((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
23 19.23v 1945 . . . . . . . . . . 11 (∀𝑥((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ (∃𝑥(𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
24 df-rex 3074 . . . . . . . . . . . 12 (∃𝑥𝐴 𝑤𝑥 ↔ ∃𝑥(𝑥𝐴𝑤𝑥))
2524imbi1i 349 . . . . . . . . . . 11 ((∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ (∃𝑥(𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
2623, 25bitr4i 277 . . . . . . . . . 10 (∀𝑥((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ (∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
2726albii 1821 . . . . . . . . 9 (∀𝑤𝑥((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑤(∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
2822, 27bitri 274 . . . . . . . 8 (∀𝑥𝑤((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑤(∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
29 df-ral 3065 . . . . . . . 8 (∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤) ↔ ∀𝑤(𝑤 𝐴 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
3021, 28, 293imtr4i 291 . . . . . . 7 (∀𝑥𝑤((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
3117, 30sylbir 234 . . . . . 6 (∀𝑥𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
3215, 31sylbi 216 . . . . 5 (∀𝑥𝐴𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
3311, 32syl 17 . . . 4 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
3433adantl 482 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
35 intssuni 4931 . . . . 5 (𝐴 ≠ ∅ → 𝐴 𝐴)
36 ssralv 4010 . . . . 5 ( 𝐴 𝐴 → (∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
3735, 36syl 17 . . . 4 (𝐴 ≠ ∅ → (∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
3837adantr 481 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
3934, 38mpd 15 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
40 dfon2lem6 34363 . . 3 ((Tr 𝐴 ∧ ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴))
41 intex 5294 . . . . . . . . . . 11 (𝐴 ≠ ∅ ↔ 𝐴 ∈ V)
42 dfon2lem3 34360 . . . . . . . . . . 11 ( 𝐴 ∈ V → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) → (Tr 𝐴 ∧ ∀𝑡 𝐴 ¬ 𝑡𝑡)))
4341, 42sylbi 216 . . . . . . . . . 10 (𝐴 ≠ ∅ → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) → (Tr 𝐴 ∧ ∀𝑡 𝐴 ¬ 𝑡𝑡)))
4443imp 407 . . . . . . . . 9 ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (Tr 𝐴 ∧ ∀𝑡 𝐴 ¬ 𝑡𝑡))
4544simprd 496 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ∀𝑡 𝐴 ¬ 𝑡𝑡)
46 untelirr 34279 . . . . . . . 8 (∀𝑡 𝐴 ¬ 𝑡𝑡 → ¬ 𝐴 𝐴)
4745, 46syl 17 . . . . . . 7 ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ¬ 𝐴 𝐴)
4847adantlr 713 . . . . . 6 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ¬ 𝐴 𝐴)
49 risset 3221 . . . . . . . . . 10 ( 𝐴𝐴 ↔ ∃𝑡𝐴 𝑡 = 𝐴)
5049notbii 319 . . . . . . . . 9 𝐴𝐴 ↔ ¬ ∃𝑡𝐴 𝑡 = 𝐴)
51 ralnex 3075 . . . . . . . . 9 (∀𝑡𝐴 ¬ 𝑡 = 𝐴 ↔ ¬ ∃𝑡𝐴 𝑡 = 𝐴)
5250, 51bitr4i 277 . . . . . . . 8 𝐴𝐴 ↔ ∀𝑡𝐴 ¬ 𝑡 = 𝐴)
53 eqcom 2743 . . . . . . . . . . . 12 (𝑡 = 𝐴 𝐴 = 𝑡)
5453notbii 319 . . . . . . . . . . 11 𝑡 = 𝐴 ↔ ¬ 𝐴 = 𝑡)
5544simpld 495 . . . . . . . . . . . . 13 ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → Tr 𝐴)
5655adantlr 713 . . . . . . . . . . . 12 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → Tr 𝐴)
57 psseq2 4048 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑡 → (𝑦𝑥𝑦𝑡))
5857anbi1d 630 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑡 → ((𝑦𝑥 ∧ Tr 𝑦) ↔ (𝑦𝑡 ∧ Tr 𝑦)))
59 elequ2 2121 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑡 → (𝑦𝑥𝑦𝑡))
6058, 59imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑡 → (((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) ↔ ((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
6160albidv 1923 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑡 → (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) ↔ ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
6261rspccv 3578 . . . . . . . . . . . . . . 15 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (𝑡𝐴 → ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
6362adantl 482 . . . . . . . . . . . . . 14 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (𝑡𝐴 → ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
64 intss1 4924 . . . . . . . . . . . . . . . 16 (𝑡𝐴 𝐴𝑡)
65 dfpss2 4045 . . . . . . . . . . . . . . . . . . . 20 ( 𝐴𝑡 ↔ ( 𝐴𝑡 ∧ ¬ 𝐴 = 𝑡))
66 psseq1 4047 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝐴 → (𝑦𝑡 𝐴𝑡))
67 treq 5230 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝐴 → (Tr 𝑦 ↔ Tr 𝐴))
6866, 67anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝐴 → ((𝑦𝑡 ∧ Tr 𝑦) ↔ ( 𝐴𝑡 ∧ Tr 𝐴)))
69 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝐴 → (𝑦𝑡 𝐴𝑡))
7068, 69imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝐴 → (((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ (( 𝐴𝑡 ∧ Tr 𝐴) → 𝐴𝑡)))
7170spcgv 3555 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝐴 ∈ V → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (( 𝐴𝑡 ∧ Tr 𝐴) → 𝐴𝑡)))
7241, 71sylbi 216 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ≠ ∅ → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (( 𝐴𝑡 ∧ Tr 𝐴) → 𝐴𝑡)))
7372imp 407 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (( 𝐴𝑡 ∧ Tr 𝐴) → 𝐴𝑡))
7473expd 416 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → ( 𝐴𝑡 → (Tr 𝐴 𝐴𝑡)))
7565, 74biimtrrid 242 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (( 𝐴𝑡 ∧ ¬ 𝐴 = 𝑡) → (Tr 𝐴 𝐴𝑡)))
7675exp4b 431 . . . . . . . . . . . . . . . . . 18 (𝐴 ≠ ∅ → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ( 𝐴𝑡 → (¬ 𝐴 = 𝑡 → (Tr 𝐴 𝐴𝑡)))))
7776com45 97 . . . . . . . . . . . . . . . . 17 (𝐴 ≠ ∅ → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ( 𝐴𝑡 → (Tr 𝐴 → (¬ 𝐴 = 𝑡 𝐴𝑡)))))
7877com23 86 . . . . . . . . . . . . . . . 16 (𝐴 ≠ ∅ → ( 𝐴𝑡 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝐴 → (¬ 𝐴 = 𝑡 𝐴𝑡)))))
7964, 78syl5 34 . . . . . . . . . . . . . . 15 (𝐴 ≠ ∅ → (𝑡𝐴 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝐴 → (¬ 𝐴 = 𝑡 𝐴𝑡)))))
8079adantr 481 . . . . . . . . . . . . . 14 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (𝑡𝐴 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝐴 → (¬ 𝐴 = 𝑡 𝐴𝑡)))))
8163, 80mpdd 43 . . . . . . . . . . . . 13 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (𝑡𝐴 → (Tr 𝐴 → (¬ 𝐴 = 𝑡 𝐴𝑡))))
8281adantr 481 . . . . . . . . . . . 12 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (𝑡𝐴 → (Tr 𝐴 → (¬ 𝐴 = 𝑡 𝐴𝑡))))
8356, 82mpid 44 . . . . . . . . . . 11 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (𝑡𝐴 → (¬ 𝐴 = 𝑡 𝐴𝑡)))
8454, 83syl7bi 254 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (𝑡𝐴 → (¬ 𝑡 = 𝐴 𝐴𝑡)))
8584ralrimiv 3142 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ∀𝑡𝐴𝑡 = 𝐴 𝐴𝑡))
86 ralim 3089 . . . . . . . . 9 (∀𝑡𝐴𝑡 = 𝐴 𝐴𝑡) → (∀𝑡𝐴 ¬ 𝑡 = 𝐴 → ∀𝑡𝐴 𝐴𝑡))
8785, 86syl 17 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (∀𝑡𝐴 ¬ 𝑡 = 𝐴 → ∀𝑡𝐴 𝐴𝑡))
8852, 87biimtrid 241 . . . . . . 7 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (¬ 𝐴𝐴 → ∀𝑡𝐴 𝐴𝑡))
89 elintg 4915 . . . . . . . . 9 ( 𝐴 ∈ V → ( 𝐴 𝐴 ↔ ∀𝑡𝐴 𝐴𝑡))
9041, 89sylbi 216 . . . . . . . 8 (𝐴 ≠ ∅ → ( 𝐴 𝐴 ↔ ∀𝑡𝐴 𝐴𝑡))
9190ad2antrr 724 . . . . . . 7 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ( 𝐴 𝐴 ↔ ∀𝑡𝐴 𝐴𝑡))
9288, 91sylibrd 258 . . . . . 6 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (¬ 𝐴𝐴 𝐴 𝐴))
9348, 92mt3d 148 . . . . 5 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → 𝐴𝐴)
9493ex 413 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) → 𝐴𝐴))
9594ancld 551 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) ∧ 𝐴𝐴)))
9640, 95syl5 34 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → ((Tr 𝐴 ∧ ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) ∧ 𝐴𝐴)))
978, 39, 96mp2and 697 1 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) ∧ 𝐴𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wal 1539   = wceq 1541  wex 1781  wcel 2106  wne 2943  wral 3064  wrex 3073  Vcvv 3445  wss 3910  wpss 3911  c0 4282   cuni 4865   cint 4907  Tr wtr 5222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-pw 4562  df-sn 4587  df-pr 4589  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-tr 5223  df-suc 6323
This theorem is referenced by:  dfon2lem9  34366
  Copyright terms: Public domain W3C validator