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 35790
Description: Lemma for dfon2 35794. 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 4097 . . . . . . . . . . . . . . . . 17 (𝑦𝑆𝑦𝑆)
2 ssralv 4051 . . . . . . . . . . . . . . . . 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 4090 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
87anbi1d 631 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → ((𝑧𝑥 ∧ Tr 𝑧) ↔ (𝑧𝑤 ∧ Tr 𝑧)))
9 elequ2 2122 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
108, 9imbi12d 344 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
1110albidv 1919 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (∀𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
1211rspccv 3618 . . . . . . . . . . . . 13 (∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → (𝑤𝑦 → ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
136, 12syl 17 . . . . . . . . . . . 12 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (𝑤𝑦 → ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
1413imp 406 . . . . . . . . . . 11 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤))
15 eldifi 4130 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (𝑆𝑦) → 𝑠𝑆)
16 psseq2 4090 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑠 → (𝑧𝑥𝑧𝑠))
1716anbi1d 631 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑠 → ((𝑧𝑥 ∧ Tr 𝑧) ↔ (𝑧𝑠 ∧ Tr 𝑧)))
18 elequ2 2122 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑠 → (𝑧𝑥𝑧𝑠))
1917, 18imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑠 → (((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2019albidv 1919 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑠 → (∀𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2120rspcv 3617 . . . . . . . . . . . . . . . 16 (𝑠𝑆 → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2215, 21syl 17 . . . . . . . . . . . . . . 15 (𝑠 ∈ (𝑆𝑦) → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
23 psseq1 4089 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑡 → (𝑧𝑠𝑡𝑠))
24 treq 5266 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑡 → (Tr 𝑧 ↔ Tr 𝑡))
2523, 24anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑡 → ((𝑧𝑠 ∧ Tr 𝑧) ↔ (𝑡𝑠 ∧ Tr 𝑡)))
26 elequ1 2114 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑡 → (𝑧𝑠𝑡𝑠))
2725, 26imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑡 → (((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) ↔ ((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)))
2827cbvalvw 2034 . . . . . . . . . . . . . . 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 3483 . . . . . . . . . . . . 13 𝑤 ∈ V
34 vex 3483 . . . . . . . . . . . . 13 𝑠 ∈ V
3533, 34dfon2lem5 35789 . . . . . . . . . . . 12 ((∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤) ∧ ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)) → (𝑤𝑠𝑤 = 𝑠𝑠𝑤))
36 3orrot 1091 . . . . . . . . . . . . . 14 ((𝑤𝑠𝑤 = 𝑠𝑠𝑤) ↔ (𝑤 = 𝑠𝑠𝑤𝑤𝑠))
37 3orass 1089 . . . . . . . . . . . . . 14 ((𝑤 = 𝑠𝑠𝑤𝑤𝑠) ↔ (𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)))
3836, 37bitri 275 . . . . . . . . . . . . 13 ((𝑤𝑠𝑤 = 𝑠𝑠𝑤) ↔ (𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)))
39 eleq1a 2835 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (𝑆𝑦) → (𝑤 = 𝑠𝑤 ∈ (𝑆𝑦)))
40 elndif 4132 . . . . . . . . . . . . . . . . . 18 (𝑤𝑦 → ¬ 𝑤 ∈ (𝑆𝑦))
4139, 40nsyli 157 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (𝑆𝑦) → (𝑤𝑦 → ¬ 𝑤 = 𝑠))
4241imp 406 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ (𝑆𝑦) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
4342adantll 714 . . . . . . . . . . . . . . 15 ((((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦)) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
4443adantll 714 . . . . . . . . . . . . . 14 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
45 orel1 888 . . . . . . . . . . . . . . 15 𝑤 = 𝑠 → ((𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)) → (𝑠𝑤𝑤𝑠)))
46 trss 5269 . . . . . . . . . . . . . . . . . . . 20 (Tr 𝑦 → (𝑤𝑦𝑤𝑦))
47 eldifn 4131 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (𝑆𝑦) → ¬ 𝑠𝑦)
48 ssel 3976 . . . . . . . . . . . . . . . . . . . . . 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 888 . . . . . . . . . . . . . . . 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 3988 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → 𝑦𝑠)
64 dfpss2 4087 . . . . . . . . 9 (𝑦𝑠 ↔ (𝑦𝑠 ∧ ¬ 𝑦 = 𝑠))
65 psseq1 4089 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → (𝑧𝑠𝑦𝑠))
66 treq 5266 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → (Tr 𝑧 ↔ Tr 𝑦))
6765, 66anbi12d 632 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → ((𝑧𝑠 ∧ Tr 𝑧) ↔ (𝑦𝑠 ∧ Tr 𝑦)))
68 elequ1 2114 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → (𝑧𝑠𝑦𝑠))
6967, 68imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦 → (((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) ↔ ((𝑦𝑠 ∧ Tr 𝑦) → 𝑦𝑠)))
7069spvv 1995 . . . . . . . . . . . . . . . 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 863 . . . . . 6 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (𝑦 = 𝑠𝑦𝑠))
8180anassrs 467 . . . . 5 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) ∧ 𝑠 ∈ (𝑆𝑦)) → (𝑦 = 𝑠𝑦𝑠))
8281ralrimiva 3145 . . . 4 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → ∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠))
83 pssdif 4368 . . . . . . 7 (𝑦𝑆 → (𝑆𝑦) ≠ ∅)
84 r19.2z 4494 . . . . . . . 8 (((𝑆𝑦) ≠ ∅ ∧ ∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠))
8584ex 412 . . . . . . 7 ((𝑆𝑦) ≠ ∅ → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
8683, 85syl 17 . . . . . 6 (𝑦𝑆 → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
8786ad2antrl 728 . . . . 5 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
88 eleq1w 2823 . . . . . . . . . 10 (𝑦 = 𝑠 → (𝑦𝑆𝑠𝑆))
8915, 88imbitrrid 246 . . . . . . . . 9 (𝑦 = 𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆))
9089a1i 11 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (𝑦 = 𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
91 trel 5267 . . . . . . . . . . 11 (Tr 𝑆 → ((𝑦𝑠𝑠𝑆) → 𝑦𝑆))
9291expd 415 . . . . . . . . . 10 (Tr 𝑆 → (𝑦𝑠 → (𝑠𝑆𝑦𝑆)))
9315, 92syl7 74 . . . . . . . . 9 (Tr 𝑆 → (𝑦𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
9493ad2antrr 726 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (𝑦𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
9590, 94jaod 859 . . . . . . 7 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → ((𝑦 = 𝑠𝑦𝑠) → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
9695com23 86 . . . . . 6 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (𝑠 ∈ (𝑆𝑦) → ((𝑦 = 𝑠𝑦𝑠) → 𝑦𝑆)))
9796rexlimdv 3152 . . . . 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 1926 1 ((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) → ∀𝑦((𝑦𝑆 ∧ Tr 𝑦) → 𝑦𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 847  w3o 1085  wal 1537  wcel 2107  wne 2939  wral 3060  wrex 3069  cdif 3947  wss 3950  wpss 3951  c0 4332  Tr wtr 5258
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431  ax-un 7756
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-pw 4601  df-sn 4626  df-pr 4628  df-uni 4907  df-iun 4992  df-tr 5259  df-suc 6389
This theorem is referenced by:  dfon2lem7  35791  dfon2lem8  35792
  Copyright terms: Public domain W3C validator