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 31449
Description: Lemma for dfon2 31451. 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 3193 . . . . . . 7 𝑥 ∈ V
2 dfon2lem3 31444 . . . . . . 7 (𝑥 ∈ V → (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (Tr 𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧𝑧)))
31, 2ax-mp 5 . . . . . 6 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (Tr 𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧𝑧))
43simpld 475 . . . . 5 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → Tr 𝑥)
54ralimi 2948 . . . 4 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑥𝐴 Tr 𝑥)
6 trint 4738 . . . 4 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
75, 6syl 17 . . 3 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → Tr 𝐴)
87adantl 482 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → Tr 𝐴)
91dfon2lem7 31448 . . . . . . 7 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
109alrimiv 1852 . . . . . 6 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
1110ralimi 2948 . . . . 5 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑥𝐴𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
12 df-ral 2913 . . . . . . 7 (∀𝑥𝐴𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑥(𝑥𝐴 → ∀𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
13 19.21v 1865 . . . . . . . 8 (∀𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))) ↔ (𝑥𝐴 → ∀𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
1413albii 1744 . . . . . . 7 (∀𝑥𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))) ↔ ∀𝑥(𝑥𝐴 → ∀𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
1512, 14bitr4i 267 . . . . . 6 (∀𝑥𝐴𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑥𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
16 impexp 462 . . . . . . . 8 (((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ (𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
17162albii 1745 . . . . . . 7 (∀𝑥𝑤((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑥𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))))
18 eluni2 4413 . . . . . . . . . . 11 (𝑤 𝐴 ↔ ∃𝑥𝐴 𝑤𝑥)
1918biimpi 206 . . . . . . . . . 10 (𝑤 𝐴 → ∃𝑥𝐴 𝑤𝑥)
2019imim1i 63 . . . . . . . . 9 ((∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → (𝑤 𝐴 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
2120alimi 1736 . . . . . . . 8 (∀𝑤(∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → ∀𝑤(𝑤 𝐴 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
22 alcom 2034 . . . . . . . . 9 (∀𝑥𝑤((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑤𝑥((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
23 19.23v 1899 . . . . . . . . . . 11 (∀𝑥((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ (∃𝑥(𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
24 df-rex 2914 . . . . . . . . . . . 12 (∃𝑥𝐴 𝑤𝑥 ↔ ∃𝑥(𝑥𝐴𝑤𝑥))
2524imbi1i 339 . . . . . . . . . . 11 ((∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ (∃𝑥(𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
2623, 25bitr4i 267 . . . . . . . . . 10 (∀𝑥((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ (∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
2726albii 1744 . . . . . . . . 9 (∀𝑤𝑥((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑤(∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
2822, 27bitri 264 . . . . . . . 8 (∀𝑥𝑤((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) ↔ ∀𝑤(∃𝑥𝐴 𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
29 df-ral 2913 . . . . . . . 8 (∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤) ↔ ∀𝑤(𝑤 𝐴 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
3021, 28, 293imtr4i 281 . . . . . . 7 (∀𝑥𝑤((𝑥𝐴𝑤𝑥) → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
3117, 30sylbir 225 . . . . . 6 (∀𝑥𝑤(𝑥𝐴 → (𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
3215, 31sylbi 207 . . . . 5 (∀𝑥𝐴𝑤(𝑤𝑥 → ∀𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
3311, 32syl 17 . . . 4 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
3433adantl 482 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
35 intssuni 4471 . . . . 5 (𝐴 ≠ ∅ → 𝐴 𝐴)
36 ssralv 3651 . . . . 5 ( 𝐴 𝐴 → (∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
3735, 36syl 17 . . . 4 (𝐴 ≠ ∅ → (∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
3837adantr 481 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)))
3934, 38mpd 15 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤))
40 dfon2lem6 31447 . . 3 ((Tr 𝐴 ∧ ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴))
41 intex 4790 . . . . . . . . . . 11 (𝐴 ≠ ∅ ↔ 𝐴 ∈ V)
42 dfon2lem3 31444 . . . . . . . . . . 11 ( 𝐴 ∈ V → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) → (Tr 𝐴 ∧ ∀𝑡 𝐴 ¬ 𝑡𝑡)))
4341, 42sylbi 207 . . . . . . . . . 10 (𝐴 ≠ ∅ → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) → (Tr 𝐴 ∧ ∀𝑡 𝐴 ¬ 𝑡𝑡)))
4443imp 445 . . . . . . . . 9 ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (Tr 𝐴 ∧ ∀𝑡 𝐴 ¬ 𝑡𝑡))
4544simprd 479 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ∀𝑡 𝐴 ¬ 𝑡𝑡)
46 untelirr 31346 . . . . . . . 8 (∀𝑡 𝐴 ¬ 𝑡𝑡 → ¬ 𝐴 𝐴)
4745, 46syl 17 . . . . . . 7 ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ¬ 𝐴 𝐴)
4847adantlr 750 . . . . . 6 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ¬ 𝐴 𝐴)
49 risset 3057 . . . . . . . . . 10 ( 𝐴𝐴 ↔ ∃𝑡𝐴 𝑡 = 𝐴)
5049notbii 310 . . . . . . . . 9 𝐴𝐴 ↔ ¬ ∃𝑡𝐴 𝑡 = 𝐴)
51 ralnex 2988 . . . . . . . . 9 (∀𝑡𝐴 ¬ 𝑡 = 𝐴 ↔ ¬ ∃𝑡𝐴 𝑡 = 𝐴)
5250, 51bitr4i 267 . . . . . . . 8 𝐴𝐴 ↔ ∀𝑡𝐴 ¬ 𝑡 = 𝐴)
53 eqcom 2628 . . . . . . . . . . . 12 (𝑡 = 𝐴 𝐴 = 𝑡)
5453notbii 310 . . . . . . . . . . 11 𝑡 = 𝐴 ↔ ¬ 𝐴 = 𝑡)
5544simpld 475 . . . . . . . . . . . . 13 ((𝐴 ≠ ∅ ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → Tr 𝐴)
5655adantlr 750 . . . . . . . . . . . 12 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → Tr 𝐴)
57 psseq2 3679 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑡 → (𝑦𝑥𝑦𝑡))
5857anbi1d 740 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑡 → ((𝑦𝑥 ∧ Tr 𝑦) ↔ (𝑦𝑡 ∧ Tr 𝑦)))
59 elequ2 2001 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑡 → (𝑦𝑥𝑦𝑡))
6058, 59imbi12d 334 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑡 → (((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) ↔ ((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
6160albidv 1846 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑡 → (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) ↔ ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
6261rspccv 3296 . . . . . . . . . . . . . . 15 (∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (𝑡𝐴 → ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
6362adantl 482 . . . . . . . . . . . . . 14 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (𝑡𝐴 → ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
64 intss1 4464 . . . . . . . . . . . . . . . 16 (𝑡𝐴 𝐴𝑡)
65 dfpss2 3676 . . . . . . . . . . . . . . . . . . . 20 ( 𝐴𝑡 ↔ ( 𝐴𝑡 ∧ ¬ 𝐴 = 𝑡))
66 psseq1 3678 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝐴 → (𝑦𝑡 𝐴𝑡))
67 treq 4728 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝐴 → (Tr 𝑦 ↔ Tr 𝐴))
6866, 67anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝐴 → ((𝑦𝑡 ∧ Tr 𝑦) ↔ ( 𝐴𝑡 ∧ Tr 𝐴)))
69 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝐴 → (𝑦𝑡 𝐴𝑡))
7068, 69imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝐴 → (((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ (( 𝐴𝑡 ∧ Tr 𝐴) → 𝐴𝑡)))
7170spcgv 3283 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝐴 ∈ V → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (( 𝐴𝑡 ∧ Tr 𝐴) → 𝐴𝑡)))
7241, 71sylbi 207 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ≠ ∅ → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (( 𝐴𝑡 ∧ Tr 𝐴) → 𝐴𝑡)))
7372imp 445 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (( 𝐴𝑡 ∧ Tr 𝐴) → 𝐴𝑡))
7473expd 452 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → ( 𝐴𝑡 → (Tr 𝐴 𝐴𝑡)))
7565, 74syl5bir 233 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ≠ ∅ ∧ ∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (( 𝐴𝑡 ∧ ¬ 𝐴 = 𝑡) → (Tr 𝐴 𝐴𝑡)))
7675exp4b 631 . . . . . . . . . . . . . . . . . 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 245 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (𝑡𝐴 → (¬ 𝑡 = 𝐴 𝐴𝑡)))
8584ralrimiv 2961 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ∀𝑡𝐴𝑡 = 𝐴 𝐴𝑡))
86 ralim 2944 . . . . . . . . 9 (∀𝑡𝐴𝑡 = 𝐴 𝐴𝑡) → (∀𝑡𝐴 ¬ 𝑡 = 𝐴 → ∀𝑡𝐴 𝐴𝑡))
8785, 86syl 17 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (∀𝑡𝐴 ¬ 𝑡 = 𝐴 → ∀𝑡𝐴 𝐴𝑡))
8852, 87syl5bi 232 . . . . . . 7 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (¬ 𝐴𝐴 → ∀𝑡𝐴 𝐴𝑡))
89 elintg 4455 . . . . . . . . 9 ( 𝐴 ∈ V → ( 𝐴 𝐴 ↔ ∀𝑡𝐴 𝐴𝑡))
9041, 89sylbi 207 . . . . . . . 8 (𝐴 ≠ ∅ → ( 𝐴 𝐴 ↔ ∀𝑡𝐴 𝐴𝑡))
9190ad2antrr 761 . . . . . . 7 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → ( 𝐴 𝐴 ↔ ∀𝑡𝐴 𝐴𝑡))
9288, 91sylibrd 249 . . . . . 6 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → (¬ 𝐴𝐴 𝐴 𝐴))
9348, 92mt3d 140 . . . . 5 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) ∧ ∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴)) → 𝐴𝐴)
9493ex 450 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) → 𝐴𝐴))
9594ancld 575 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) ∧ 𝐴𝐴)))
9640, 95syl5 34 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → ((Tr 𝐴 ∧ ∀𝑤 𝐴𝑡((𝑡𝑤 ∧ Tr 𝑡) → 𝑡𝑤)) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) ∧ 𝐴𝐴)))
978, 39, 96mp2and 714 1 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)) → (∀𝑧((𝑧 𝐴 ∧ Tr 𝑧) → 𝑧 𝐴) ∧ 𝐴𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  wal 1478   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2908  wrex 2909  Vcvv 3190  wss 3560  wpss 3561  c0 3897   cuni 4409   cint 4447  Tr wtr 4722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877  ax-un 6914
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-pw 4138  df-sn 4156  df-pr 4158  df-uni 4410  df-int 4448  df-iun 4494  df-tr 4723  df-suc 5698
This theorem is referenced by:  dfon2lem9  31450
  Copyright terms: Public domain W3C validator