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 34760
Description: Lemma for dfon2 34764. 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 4096 . . . . . . . . . . . . . . . . 17 (𝑦𝑆𝑦𝑆)
2 ssralv 4051 . . . . . . . . . . . . . . . . 17 (𝑦𝑆 → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)))
31, 2syl 17 . . . . . . . . . . . . . . . 16 (𝑦𝑆 → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)))
43impcom 409 . . . . . . . . . . . . . . 15 ((∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ∧ 𝑦𝑆) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥))
54adantrr 716 . . . . . . . . . . . . . 14 ((∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥))
65ad2ant2lr 747 . . . . . . . . . . . . 13 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥))
7 psseq2 4089 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
87anbi1d 631 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → ((𝑧𝑥 ∧ Tr 𝑧) ↔ (𝑧𝑤 ∧ Tr 𝑧)))
9 elequ2 2122 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
108, 9imbi12d 345 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
1110albidv 1924 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (∀𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
1211rspccv 3610 . . . . . . . . . . . . 13 (∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → (𝑤𝑦 → ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
136, 12syl 17 . . . . . . . . . . . 12 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (𝑤𝑦 → ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
1413imp 408 . . . . . . . . . . 11 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤))
15 eldifi 4127 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (𝑆𝑦) → 𝑠𝑆)
16 psseq2 4089 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑠 → (𝑧𝑥𝑧𝑠))
1716anbi1d 631 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑠 → ((𝑧𝑥 ∧ Tr 𝑧) ↔ (𝑧𝑠 ∧ Tr 𝑧)))
18 elequ2 2122 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑠 → (𝑧𝑥𝑧𝑠))
1917, 18imbi12d 345 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑠 → (((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2019albidv 1924 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑠 → (∀𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2120rspcv 3609 . . . . . . . . . . . . . . . 16 (𝑠𝑆 → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2215, 21syl 17 . . . . . . . . . . . . . . 15 (𝑠 ∈ (𝑆𝑦) → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
23 psseq1 4088 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑡 → (𝑧𝑠𝑡𝑠))
24 treq 5274 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑡 → (Tr 𝑧 ↔ Tr 𝑡))
2523, 24anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑡 → ((𝑧𝑠 ∧ Tr 𝑧) ↔ (𝑡𝑠 ∧ Tr 𝑡)))
26 elequ1 2114 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑡 → (𝑧𝑠𝑡𝑠))
2725, 26imbi12d 345 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑡 → (((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) ↔ ((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)))
2827cbvalvw 2040 . . . . . . . . . . . . . . 15 (∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) ↔ ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠))
2922, 28imbitrdi 250 . . . . . . . . . . . . . 14 (𝑠 ∈ (𝑆𝑦) → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)))
3029impcom 409 . . . . . . . . . . . . 13 ((∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ∧ 𝑠 ∈ (𝑆𝑦)) → ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠))
3130ad2ant2l 745 . . . . . . . . . . . 12 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠))
3231adantr 482 . . . . . . . . . . 11 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠))
33 vex 3479 . . . . . . . . . . . . 13 𝑤 ∈ V
34 vex 3479 . . . . . . . . . . . . 13 𝑠 ∈ V
3533, 34dfon2lem5 34759 . . . . . . . . . . . 12 ((∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤) ∧ ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)) → (𝑤𝑠𝑤 = 𝑠𝑠𝑤))
36 3orrot 1093 . . . . . . . . . . . . . 14 ((𝑤𝑠𝑤 = 𝑠𝑠𝑤) ↔ (𝑤 = 𝑠𝑠𝑤𝑤𝑠))
37 3orass 1091 . . . . . . . . . . . . . 14 ((𝑤 = 𝑠𝑠𝑤𝑤𝑠) ↔ (𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)))
3836, 37bitri 275 . . . . . . . . . . . . 13 ((𝑤𝑠𝑤 = 𝑠𝑠𝑤) ↔ (𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)))
39 eleq1a 2829 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (𝑆𝑦) → (𝑤 = 𝑠𝑤 ∈ (𝑆𝑦)))
40 elndif 4129 . . . . . . . . . . . . . . . . . 18 (𝑤𝑦 → ¬ 𝑤 ∈ (𝑆𝑦))
4139, 40nsyli 157 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (𝑆𝑦) → (𝑤𝑦 → ¬ 𝑤 = 𝑠))
4241imp 408 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ (𝑆𝑦) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
4342adantll 713 . . . . . . . . . . . . . . 15 ((((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦)) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
4443adantll 713 . . . . . . . . . . . . . 14 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
45 orel1 888 . . . . . . . . . . . . . . 15 𝑤 = 𝑠 → ((𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)) → (𝑠𝑤𝑤𝑠)))
46 trss 5277 . . . . . . . . . . . . . . . . . . . 20 (Tr 𝑦 → (𝑤𝑦𝑤𝑦))
47 eldifn 4128 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (𝑆𝑦) → ¬ 𝑠𝑦)
48 ssel 3976 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤𝑦 → (𝑠𝑤𝑠𝑦))
4948con3d 152 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑦 → (¬ 𝑠𝑦 → ¬ 𝑠𝑤))
5047, 49syl5com 31 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (𝑆𝑦) → (𝑤𝑦 → ¬ 𝑠𝑤))
5146, 50syl9 77 . . . . . . . . . . . . . . . . . . 19 (Tr 𝑦 → (𝑠 ∈ (𝑆𝑦) → (𝑤𝑦 → ¬ 𝑠𝑤)))
5251adantl 483 . . . . . . . . . . . . . . . . . 18 ((𝑦𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆𝑦) → (𝑤𝑦 → ¬ 𝑠𝑤)))
5352imp31 419 . . . . . . . . . . . . . . . . 17 ((((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦)) ∧ 𝑤𝑦) → ¬ 𝑠𝑤)
5453adantll 713 . . . . . . . . . . . . . . . 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 241 . . . . . . . . . . . 12 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ((𝑤𝑠𝑤 = 𝑠𝑠𝑤) → 𝑤𝑠))
6035, 59syl5 34 . . . . . . . . . . 11 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ((∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤) ∧ ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)) → 𝑤𝑠))
6114, 32, 60mp2and 698 . . . . . . . . . 10 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → 𝑤𝑠)
6261ex 414 . . . . . . . . 9 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (𝑤𝑦𝑤𝑠))
6362ssrdv 3989 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → 𝑦𝑠)
64 dfpss2 4086 . . . . . . . . 9 (𝑦𝑠 ↔ (𝑦𝑠 ∧ ¬ 𝑦 = 𝑠))
65 psseq1 4088 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → (𝑧𝑠𝑦𝑠))
66 treq 5274 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → (Tr 𝑧 ↔ Tr 𝑦))
6765, 66anbi12d 632 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → ((𝑧𝑠 ∧ Tr 𝑧) ↔ (𝑦𝑠 ∧ Tr 𝑦)))
68 elequ1 2114 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → (𝑧𝑠𝑦𝑠))
6967, 68imbi12d 345 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦 → (((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) ↔ ((𝑦𝑠 ∧ Tr 𝑦) → 𝑦𝑠)))
7069spvv 2001 . . . . . . . . . . . . . . . 16 (∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) → ((𝑦𝑠 ∧ Tr 𝑦) → 𝑦𝑠))
7170expd 417 . . . . . . . . . . . . . . 15 (∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) → (𝑦𝑠 → (Tr 𝑦𝑦𝑠)))
7271com23 86 . . . . . . . . . . . . . 14 (∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) → (Tr 𝑦 → (𝑦𝑠𝑦𝑠)))
7322, 72syl6 35 . . . . . . . . . . . . 13 (𝑠 ∈ (𝑆𝑦) → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → (Tr 𝑦 → (𝑦𝑠𝑦𝑠))))
7473com3l 89 . . . . . . . . . . . 12 (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → (Tr 𝑦 → (𝑠 ∈ (𝑆𝑦) → (𝑦𝑠𝑦𝑠))))
7574adantld 492 . . . . . . . . . . 11 (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ((𝑦𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆𝑦) → (𝑦𝑠𝑦𝑠))))
7675adantl 483 . . . . . . . . . 10 ((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) → ((𝑦𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆𝑦) → (𝑦𝑠𝑦𝑠))))
7776imp32 420 . . . . . . . . 9 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (𝑦𝑠𝑦𝑠))
7864, 77biimtrrid 242 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → ((𝑦𝑠 ∧ ¬ 𝑦 = 𝑠) → 𝑦𝑠))
7963, 78mpand 694 . . . . . . 7 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (¬ 𝑦 = 𝑠𝑦𝑠))
8079orrd 862 . . . . . 6 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (𝑦 = 𝑠𝑦𝑠))
8180anassrs 469 . . . . 5 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) ∧ 𝑠 ∈ (𝑆𝑦)) → (𝑦 = 𝑠𝑦𝑠))
8281ralrimiva 3147 . . . 4 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → ∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠))
83 pssdif 4367 . . . . . . 7 (𝑦𝑆 → (𝑆𝑦) ≠ ∅)
84 r19.2z 4495 . . . . . . . 8 (((𝑆𝑦) ≠ ∅ ∧ ∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠))
8584ex 414 . . . . . . 7 ((𝑆𝑦) ≠ ∅ → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
8683, 85syl 17 . . . . . 6 (𝑦𝑆 → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
8786ad2antrl 727 . . . . 5 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
88 eleq1w 2817 . . . . . . . . . 10 (𝑦 = 𝑠 → (𝑦𝑆𝑠𝑆))
8915, 88imbitrrid 245 . . . . . . . . 9 (𝑦 = 𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆))
9089a1i 11 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (𝑦 = 𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
91 trel 5275 . . . . . . . . . . 11 (Tr 𝑆 → ((𝑦𝑠𝑠𝑆) → 𝑦𝑆))
9291expd 417 . . . . . . . . . 10 (Tr 𝑆 → (𝑦𝑠 → (𝑠𝑆𝑦𝑆)))
9315, 92syl7 74 . . . . . . . . 9 (Tr 𝑆 → (𝑦𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
9493ad2antrr 725 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (𝑦𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
9590, 94jaod 858 . . . . . . 7 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → ((𝑦 = 𝑠𝑦𝑠) → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
9695com23 86 . . . . . 6 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (𝑠 ∈ (𝑆𝑦) → ((𝑦 = 𝑠𝑦𝑠) → 𝑦𝑆)))
9796rexlimdv 3154 . . . . 5 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → 𝑦𝑆))
9887, 97syld 47 . . . 4 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → 𝑦𝑆))
9982, 98mpd 15 . . 3 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → 𝑦𝑆)
10099ex 414 . 2 ((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) → ((𝑦𝑆 ∧ Tr 𝑦) → 𝑦𝑆))
101100alrimiv 1931 1 ((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) → ∀𝑦((𝑦𝑆 ∧ Tr 𝑦) → 𝑦𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wo 846  w3o 1087  wal 1540  wcel 2107  wne 2941  wral 3062  wrex 3071  cdif 3946  wss 3949  wpss 3950  c0 4323  Tr wtr 5266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-pw 4605  df-sn 4630  df-pr 4632  df-uni 4910  df-iun 5000  df-tr 5267  df-suc 6371
This theorem is referenced by:  dfon2lem7  34761  dfon2lem8  34762
  Copyright terms: Public domain W3C validator