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

Theorem dfon2lem6 35789
Description: Lemma for dfon2 35793. A transitive class of sets satisfying the new definition satisfies the new definition. (Contributed by Scott Fenton, 25-Feb-2011.)
Assertion
Ref Expression
dfon2lem6 ((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) → ∀𝑦((𝑦𝑆 ∧ Tr 𝑦) → 𝑦𝑆))
Distinct variable group:   𝑥,𝑆,𝑦,𝑧

Proof of Theorem dfon2lem6
Dummy variables 𝑤 𝑠 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pssss 4098 . . . . . . . . . . . . . . . . 17 (𝑦𝑆𝑦𝑆)
2 ssralv 4052 . . . . . . . . . . . . . . . . 17 (𝑦𝑆 → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)))
31, 2syl 17 . . . . . . . . . . . . . . . 16 (𝑦𝑆 → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)))
43impcom 407 . . . . . . . . . . . . . . 15 ((∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ∧ 𝑦𝑆) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥))
54adantrr 717 . . . . . . . . . . . . . 14 ((∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥))
65ad2ant2lr 748 . . . . . . . . . . . . 13 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥))
7 psseq2 4091 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
87anbi1d 631 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → ((𝑧𝑥 ∧ Tr 𝑧) ↔ (𝑧𝑤 ∧ Tr 𝑧)))
9 elequ2 2123 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
108, 9imbi12d 344 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
1110albidv 1920 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (∀𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
1211rspccv 3619 . . . . . . . . . . . . 13 (∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → (𝑤𝑦 → ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
136, 12syl 17 . . . . . . . . . . . 12 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (𝑤𝑦 → ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
1413imp 406 . . . . . . . . . . 11 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤))
15 eldifi 4131 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (𝑆𝑦) → 𝑠𝑆)
16 psseq2 4091 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑠 → (𝑧𝑥𝑧𝑠))
1716anbi1d 631 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑠 → ((𝑧𝑥 ∧ Tr 𝑧) ↔ (𝑧𝑠 ∧ Tr 𝑧)))
18 elequ2 2123 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑠 → (𝑧𝑥𝑧𝑠))
1917, 18imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑠 → (((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2019albidv 1920 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑠 → (∀𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2120rspcv 3618 . . . . . . . . . . . . . . . 16 (𝑠𝑆 → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2215, 21syl 17 . . . . . . . . . . . . . . 15 (𝑠 ∈ (𝑆𝑦) → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
23 psseq1 4090 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑡 → (𝑧𝑠𝑡𝑠))
24 treq 5267 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑡 → (Tr 𝑧 ↔ Tr 𝑡))
2523, 24anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑡 → ((𝑧𝑠 ∧ Tr 𝑧) ↔ (𝑡𝑠 ∧ Tr 𝑡)))
26 elequ1 2115 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑡 → (𝑧𝑠𝑡𝑠))
2725, 26imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑡 → (((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) ↔ ((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)))
2827cbvalvw 2035 . . . . . . . . . . . . . . 15 (∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) ↔ ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠))
2922, 28imbitrdi 251 . . . . . . . . . . . . . 14 (𝑠 ∈ (𝑆𝑦) → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)))
3029impcom 407 . . . . . . . . . . . . 13 ((∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ∧ 𝑠 ∈ (𝑆𝑦)) → ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠))
3130ad2ant2l 746 . . . . . . . . . . . 12 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠))
3231adantr 480 . . . . . . . . . . 11 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠))
33 vex 3484 . . . . . . . . . . . . 13 𝑤 ∈ V
34 vex 3484 . . . . . . . . . . . . 13 𝑠 ∈ V
3533, 34dfon2lem5 35788 . . . . . . . . . . . 12 ((∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤) ∧ ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)) → (𝑤𝑠𝑤 = 𝑠𝑠𝑤))
36 3orrot 1092 . . . . . . . . . . . . . 14 ((𝑤𝑠𝑤 = 𝑠𝑠𝑤) ↔ (𝑤 = 𝑠𝑠𝑤𝑤𝑠))
37 3orass 1090 . . . . . . . . . . . . . 14 ((𝑤 = 𝑠𝑠𝑤𝑤𝑠) ↔ (𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)))
3836, 37bitri 275 . . . . . . . . . . . . 13 ((𝑤𝑠𝑤 = 𝑠𝑠𝑤) ↔ (𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)))
39 eleq1a 2836 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (𝑆𝑦) → (𝑤 = 𝑠𝑤 ∈ (𝑆𝑦)))
40 elndif 4133 . . . . . . . . . . . . . . . . . 18 (𝑤𝑦 → ¬ 𝑤 ∈ (𝑆𝑦))
4139, 40nsyli 157 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (𝑆𝑦) → (𝑤𝑦 → ¬ 𝑤 = 𝑠))
4241imp 406 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ (𝑆𝑦) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
4342adantll 714 . . . . . . . . . . . . . . 15 ((((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦)) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
4443adantll 714 . . . . . . . . . . . . . 14 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
45 orel1 889 . . . . . . . . . . . . . . 15 𝑤 = 𝑠 → ((𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)) → (𝑠𝑤𝑤𝑠)))
46 trss 5270 . . . . . . . . . . . . . . . . . . . 20 (Tr 𝑦 → (𝑤𝑦𝑤𝑦))
47 eldifn 4132 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (𝑆𝑦) → ¬ 𝑠𝑦)
48 ssel 3977 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤𝑦 → (𝑠𝑤𝑠𝑦))
4948con3d 152 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑦 → (¬ 𝑠𝑦 → ¬ 𝑠𝑤))
5047, 49syl5com 31 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (𝑆𝑦) → (𝑤𝑦 → ¬ 𝑠𝑤))
5146, 50syl9 77 . . . . . . . . . . . . . . . . . . 19 (Tr 𝑦 → (𝑠 ∈ (𝑆𝑦) → (𝑤𝑦 → ¬ 𝑠𝑤)))
5251adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑦𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆𝑦) → (𝑤𝑦 → ¬ 𝑠𝑤)))
5352imp31 417 . . . . . . . . . . . . . . . . 17 ((((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦)) ∧ 𝑤𝑦) → ¬ 𝑠𝑤)
5453adantll 714 . . . . . . . . . . . . . . . 16 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ¬ 𝑠𝑤)
55 orel1 889 . . . . . . . . . . . . . . . 16 𝑠𝑤 → ((𝑠𝑤𝑤𝑠) → 𝑤𝑠))
5654, 55syl 17 . . . . . . . . . . . . . . 15 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ((𝑠𝑤𝑤𝑠) → 𝑤𝑠))
5745, 56syl9r 78 . . . . . . . . . . . . . 14 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → (¬ 𝑤 = 𝑠 → ((𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)) → 𝑤𝑠)))
5844, 57mpd 15 . . . . . . . . . . . . 13 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ((𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)) → 𝑤𝑠))
5938, 58biimtrid 242 . . . . . . . . . . . 12 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ((𝑤𝑠𝑤 = 𝑠𝑠𝑤) → 𝑤𝑠))
6035, 59syl5 34 . . . . . . . . . . 11 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ((∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤) ∧ ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)) → 𝑤𝑠))
6114, 32, 60mp2and 699 . . . . . . . . . 10 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → 𝑤𝑠)
6261ex 412 . . . . . . . . 9 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (𝑤𝑦𝑤𝑠))
6362ssrdv 3989 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → 𝑦𝑠)
64 dfpss2 4088 . . . . . . . . 9 (𝑦𝑠 ↔ (𝑦𝑠 ∧ ¬ 𝑦 = 𝑠))
65 psseq1 4090 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → (𝑧𝑠𝑦𝑠))
66 treq 5267 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → (Tr 𝑧 ↔ Tr 𝑦))
6765, 66anbi12d 632 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → ((𝑧𝑠 ∧ Tr 𝑧) ↔ (𝑦𝑠 ∧ Tr 𝑦)))
68 elequ1 2115 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → (𝑧𝑠𝑦𝑠))
6967, 68imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦 → (((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) ↔ ((𝑦𝑠 ∧ Tr 𝑦) → 𝑦𝑠)))
7069spvv 1996 . . . . . . . . . . . . . . . 16 (∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) → ((𝑦𝑠 ∧ Tr 𝑦) → 𝑦𝑠))
7170expd 415 . . . . . . . . . . . . . . 15 (∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) → (𝑦𝑠 → (Tr 𝑦𝑦𝑠)))
7271com23 86 . . . . . . . . . . . . . 14 (∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) → (Tr 𝑦 → (𝑦𝑠𝑦𝑠)))
7322, 72syl6 35 . . . . . . . . . . . . 13 (𝑠 ∈ (𝑆𝑦) → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → (Tr 𝑦 → (𝑦𝑠𝑦𝑠))))
7473com3l 89 . . . . . . . . . . . 12 (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → (Tr 𝑦 → (𝑠 ∈ (𝑆𝑦) → (𝑦𝑠𝑦𝑠))))
7574adantld 490 . . . . . . . . . . 11 (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ((𝑦𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆𝑦) → (𝑦𝑠𝑦𝑠))))
7675adantl 481 . . . . . . . . . 10 ((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) → ((𝑦𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆𝑦) → (𝑦𝑠𝑦𝑠))))
7776imp32 418 . . . . . . . . 9 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (𝑦𝑠𝑦𝑠))
7864, 77biimtrrid 243 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → ((𝑦𝑠 ∧ ¬ 𝑦 = 𝑠) → 𝑦𝑠))
7963, 78mpand 695 . . . . . . 7 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (¬ 𝑦 = 𝑠𝑦𝑠))
8079orrd 864 . . . . . 6 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (𝑦 = 𝑠𝑦𝑠))
8180anassrs 467 . . . . 5 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) ∧ 𝑠 ∈ (𝑆𝑦)) → (𝑦 = 𝑠𝑦𝑠))
8281ralrimiva 3146 . . . 4 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → ∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠))
83 pssdif 4369 . . . . . . 7 (𝑦𝑆 → (𝑆𝑦) ≠ ∅)
84 r19.2z 4495 . . . . . . . 8 (((𝑆𝑦) ≠ ∅ ∧ ∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠))
8584ex 412 . . . . . . 7 ((𝑆𝑦) ≠ ∅ → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
8683, 85syl 17 . . . . . 6 (𝑦𝑆 → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
8786ad2antrl 728 . . . . 5 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
88 eleq1w 2824 . . . . . . . . . 10 (𝑦 = 𝑠 → (𝑦𝑆𝑠𝑆))
8915, 88imbitrrid 246 . . . . . . . . 9 (𝑦 = 𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆))
9089a1i 11 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (𝑦 = 𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
91 trel 5268 . . . . . . . . . . 11 (Tr 𝑆 → ((𝑦𝑠𝑠𝑆) → 𝑦𝑆))
9291expd 415 . . . . . . . . . 10 (Tr 𝑆 → (𝑦𝑠 → (𝑠𝑆𝑦𝑆)))
9315, 92syl7 74 . . . . . . . . 9 (Tr 𝑆 → (𝑦𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
9493ad2antrr 726 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (𝑦𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
9590, 94jaod 860 . . . . . . 7 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → ((𝑦 = 𝑠𝑦𝑠) → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
9695com23 86 . . . . . 6 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (𝑠 ∈ (𝑆𝑦) → ((𝑦 = 𝑠𝑦𝑠) → 𝑦𝑆)))
9796rexlimdv 3153 . . . . 5 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → 𝑦𝑆))
9887, 97syld 47 . . . 4 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → 𝑦𝑆))
9982, 98mpd 15 . . 3 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → 𝑦𝑆)
10099ex 412 . 2 ((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) → ((𝑦𝑆 ∧ Tr 𝑦) → 𝑦𝑆))
101100alrimiv 1927 1 ((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) → ∀𝑦((𝑦𝑆 ∧ Tr 𝑦) → 𝑦𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 848  w3o 1086  wal 1538  wcel 2108  wne 2940  wral 3061  wrex 3070  cdif 3948  wss 3951  wpss 3952  c0 4333  Tr wtr 5259
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-pw 4602  df-sn 4627  df-pr 4629  df-uni 4908  df-iun 4993  df-tr 5260  df-suc 6390
This theorem is referenced by:  dfon2lem7  35790  dfon2lem8  35791
  Copyright terms: Public domain W3C validator