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 35769
Description: Lemma for dfon2 35773. 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 4107 . . . . . . . . . . . . . . . . 17 (𝑦𝑆𝑦𝑆)
2 ssralv 4063 . . . . . . . . . . . . . . . . 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 4100 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
87anbi1d 631 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → ((𝑧𝑥 ∧ Tr 𝑧) ↔ (𝑧𝑤 ∧ Tr 𝑧)))
9 elequ2 2120 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
108, 9imbi12d 344 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
1110albidv 1917 . . . . . . . . . . . . . 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 4140 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (𝑆𝑦) → 𝑠𝑆)
16 psseq2 4100 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑠 → (𝑧𝑥𝑧𝑠))
1716anbi1d 631 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑠 → ((𝑧𝑥 ∧ Tr 𝑧) ↔ (𝑧𝑠 ∧ Tr 𝑧)))
18 elequ2 2120 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑠 → (𝑧𝑥𝑧𝑠))
1917, 18imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑠 → (((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2019albidv 1917 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑠 → (∀𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2120rspcv 3617 . . . . . . . . . . . . . . . 16 (𝑠𝑆 → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2215, 21syl 17 . . . . . . . . . . . . . . 15 (𝑠 ∈ (𝑆𝑦) → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
23 psseq1 4099 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑡 → (𝑧𝑠𝑡𝑠))
24 treq 5272 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑡 → (Tr 𝑧 ↔ Tr 𝑡))
2523, 24anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑡 → ((𝑧𝑠 ∧ Tr 𝑧) ↔ (𝑡𝑠 ∧ Tr 𝑡)))
26 elequ1 2112 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑡 → (𝑧𝑠𝑡𝑠))
2725, 26imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑡 → (((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) ↔ ((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)))
2827cbvalvw 2032 . . . . . . . . . . . . . . 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 3481 . . . . . . . . . . . . 13 𝑤 ∈ V
34 vex 3481 . . . . . . . . . . . . 13 𝑠 ∈ V
3533, 34dfon2lem5 35768 . . . . . . . . . . . 12 ((∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤) ∧ ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)) → (𝑤𝑠𝑤 = 𝑠𝑠𝑤))
36 3orrot 1091 . . . . . . . . . . . . . 14 ((𝑤𝑠𝑤 = 𝑠𝑠𝑤) ↔ (𝑤 = 𝑠𝑠𝑤𝑤𝑠))
37 3orass 1089 . . . . . . . . . . . . . 14 ((𝑤 = 𝑠𝑠𝑤𝑤𝑠) ↔ (𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)))
3836, 37bitri 275 . . . . . . . . . . . . 13 ((𝑤𝑠𝑤 = 𝑠𝑠𝑤) ↔ (𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)))
39 eleq1a 2833 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (𝑆𝑦) → (𝑤 = 𝑠𝑤 ∈ (𝑆𝑦)))
40 elndif 4142 . . . . . . . . . . . . . . . . . 18 (𝑤𝑦 → ¬ 𝑤 ∈ (𝑆𝑦))
4139, 40nsyli 157 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (𝑆𝑦) → (𝑤𝑦 → ¬ 𝑤 = 𝑠))
4241imp 406 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ (𝑆𝑦) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
4342adantll 714 . . . . . . . . . . . . . . 15 ((((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦)) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
4443adantll 714 . . . . . . . . . . . . . 14 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
45 orel1 888 . . . . . . . . . . . . . . 15 𝑤 = 𝑠 → ((𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)) → (𝑠𝑤𝑤𝑠)))
46 trss 5275 . . . . . . . . . . . . . . . . . . . 20 (Tr 𝑦 → (𝑤𝑦𝑤𝑦))
47 eldifn 4141 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (𝑆𝑦) → ¬ 𝑠𝑦)
48 ssel 3988 . . . . . . . . . . . . . . . . . . . . . 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 4000 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → 𝑦𝑠)
64 dfpss2 4097 . . . . . . . . 9 (𝑦𝑠 ↔ (𝑦𝑠 ∧ ¬ 𝑦 = 𝑠))
65 psseq1 4099 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → (𝑧𝑠𝑦𝑠))
66 treq 5272 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → (Tr 𝑧 ↔ Tr 𝑦))
6765, 66anbi12d 632 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → ((𝑧𝑠 ∧ Tr 𝑧) ↔ (𝑦𝑠 ∧ Tr 𝑦)))
68 elequ1 2112 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → (𝑧𝑠𝑦𝑠))
6967, 68imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦 → (((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) ↔ ((𝑦𝑠 ∧ Tr 𝑦) → 𝑦𝑠)))
7069spvv 1993 . . . . . . . . . . . . . . . 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 3143 . . . 4 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → ∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠))
83 pssdif 4374 . . . . . . 7 (𝑦𝑆 → (𝑆𝑦) ≠ ∅)
84 r19.2z 4500 . . . . . . . 8 (((𝑆𝑦) ≠ ∅ ∧ ∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠))
8584ex 412 . . . . . . 7 ((𝑆𝑦) ≠ ∅ → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
8683, 85syl 17 . . . . . 6 (𝑦𝑆 → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
8786ad2antrl 728 . . . . 5 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
88 eleq1w 2821 . . . . . . . . . 10 (𝑦 = 𝑠 → (𝑦𝑆𝑠𝑆))
8915, 88imbitrrid 246 . . . . . . . . 9 (𝑦 = 𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆))
9089a1i 11 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (𝑦 = 𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
91 trel 5273 . . . . . . . . . . 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 3150 . . . . 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 1924 1 ((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) → ∀𝑦((𝑦𝑆 ∧ Tr 𝑦) → 𝑦𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 847  w3o 1085  wal 1534  wcel 2105  wne 2937  wral 3058  wrex 3067  cdif 3959  wss 3962  wpss 3963  c0 4338  Tr wtr 5264
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-pw 4606  df-sn 4631  df-pr 4633  df-uni 4912  df-iun 4997  df-tr 5265  df-suc 6391
This theorem is referenced by:  dfon2lem7  35770  dfon2lem8  35771
  Copyright terms: Public domain W3C validator