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 32930
Description: Lemma for dfon2 32934. 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 4069 . . . . . . . . . . . . . . . . 17 (𝑦𝑆𝑦𝑆)
2 ssralv 4030 . . . . . . . . . . . . . . . . 17 (𝑦𝑆 → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)))
31, 2syl 17 . . . . . . . . . . . . . . . 16 (𝑦𝑆 → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)))
43impcom 408 . . . . . . . . . . . . . . 15 ((∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ∧ 𝑦𝑆) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥))
54adantrr 713 . . . . . . . . . . . . . 14 ((∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥))
65ad2ant2lr 744 . . . . . . . . . . . . 13 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → ∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥))
7 psseq2 4062 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
87anbi1d 629 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → ((𝑧𝑥 ∧ Tr 𝑧) ↔ (𝑧𝑤 ∧ Tr 𝑧)))
9 elequ2 2120 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
108, 9imbi12d 346 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
1110albidv 1912 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (∀𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
1211rspccv 3617 . . . . . . . . . . . . 13 (∀𝑥𝑦𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → (𝑤𝑦 → ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
136, 12syl 17 . . . . . . . . . . . 12 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (𝑤𝑦 → ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤)))
1413imp 407 . . . . . . . . . . 11 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤))
15 eldifi 4100 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (𝑆𝑦) → 𝑠𝑆)
16 psseq2 4062 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑠 → (𝑧𝑥𝑧𝑠))
1716anbi1d 629 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑠 → ((𝑧𝑥 ∧ Tr 𝑧) ↔ (𝑧𝑠 ∧ Tr 𝑧)))
18 elequ2 2120 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑠 → (𝑧𝑥𝑧𝑠))
1917, 18imbi12d 346 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑠 → (((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2019albidv 1912 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑠 → (∀𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ↔ ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2120rspcv 3615 . . . . . . . . . . . . . . . 16 (𝑠𝑆 → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
2215, 21syl 17 . . . . . . . . . . . . . . 15 (𝑠 ∈ (𝑆𝑦) → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠)))
23 psseq1 4061 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑡 → (𝑧𝑠𝑡𝑠))
24 treq 5169 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑡 → (Tr 𝑧 ↔ Tr 𝑡))
2523, 24anbi12d 630 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑡 → ((𝑧𝑠 ∧ Tr 𝑧) ↔ (𝑡𝑠 ∧ Tr 𝑡)))
26 elequ1 2112 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑡 → (𝑧𝑠𝑡𝑠))
2725, 26imbi12d 346 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑡 → (((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) ↔ ((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)))
2827cbvalvw 2034 . . . . . . . . . . . . . . 15 (∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) ↔ ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠))
2922, 28syl6ib 252 . . . . . . . . . . . . . 14 (𝑠 ∈ (𝑆𝑦) → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)))
3029impcom 408 . . . . . . . . . . . . 13 ((∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) ∧ 𝑠 ∈ (𝑆𝑦)) → ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠))
3130ad2ant2l 742 . . . . . . . . . . . 12 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠))
3231adantr 481 . . . . . . . . . . 11 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠))
33 vex 3495 . . . . . . . . . . . . 13 𝑤 ∈ V
34 vex 3495 . . . . . . . . . . . . 13 𝑠 ∈ V
3533, 34dfon2lem5 32929 . . . . . . . . . . . 12 ((∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤) ∧ ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)) → (𝑤𝑠𝑤 = 𝑠𝑠𝑤))
36 3orrot 1084 . . . . . . . . . . . . . 14 ((𝑤𝑠𝑤 = 𝑠𝑠𝑤) ↔ (𝑤 = 𝑠𝑠𝑤𝑤𝑠))
37 3orass 1082 . . . . . . . . . . . . . 14 ((𝑤 = 𝑠𝑠𝑤𝑤𝑠) ↔ (𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)))
3836, 37bitri 276 . . . . . . . . . . . . 13 ((𝑤𝑠𝑤 = 𝑠𝑠𝑤) ↔ (𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)))
39 eleq1a 2905 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (𝑆𝑦) → (𝑤 = 𝑠𝑤 ∈ (𝑆𝑦)))
40 elndif 4102 . . . . . . . . . . . . . . . . . 18 (𝑤𝑦 → ¬ 𝑤 ∈ (𝑆𝑦))
4139, 40nsyli 160 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (𝑆𝑦) → (𝑤𝑦 → ¬ 𝑤 = 𝑠))
4241imp 407 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ (𝑆𝑦) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
4342adantll 710 . . . . . . . . . . . . . . 15 ((((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦)) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
4443adantll 710 . . . . . . . . . . . . . 14 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ¬ 𝑤 = 𝑠)
45 orel1 882 . . . . . . . . . . . . . . 15 𝑤 = 𝑠 → ((𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)) → (𝑠𝑤𝑤𝑠)))
46 trss 5172 . . . . . . . . . . . . . . . . . . . 20 (Tr 𝑦 → (𝑤𝑦𝑤𝑦))
47 eldifn 4101 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (𝑆𝑦) → ¬ 𝑠𝑦)
48 ssel 3958 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤𝑦 → (𝑠𝑤𝑠𝑦))
4948con3d 155 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑦 → (¬ 𝑠𝑦 → ¬ 𝑠𝑤))
5047, 49syl5com 31 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (𝑆𝑦) → (𝑤𝑦 → ¬ 𝑠𝑤))
5146, 50syl9 77 . . . . . . . . . . . . . . . . . . 19 (Tr 𝑦 → (𝑠 ∈ (𝑆𝑦) → (𝑤𝑦 → ¬ 𝑠𝑤)))
5251adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑦𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆𝑦) → (𝑤𝑦 → ¬ 𝑠𝑤)))
5352imp31 418 . . . . . . . . . . . . . . . . 17 ((((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦)) ∧ 𝑤𝑦) → ¬ 𝑠𝑤)
5453adantll 710 . . . . . . . . . . . . . . . 16 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ¬ 𝑠𝑤)
55 orel1 882 . . . . . . . . . . . . . . . 16 𝑠𝑤 → ((𝑠𝑤𝑤𝑠) → 𝑤𝑠))
5654, 55syl 17 . . . . . . . . . . . . . . 15 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ((𝑠𝑤𝑤𝑠) → 𝑤𝑠))
5745, 56syl9r 78 . . . . . . . . . . . . . 14 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → (¬ 𝑤 = 𝑠 → ((𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)) → 𝑤𝑠)))
5844, 57mpd 15 . . . . . . . . . . . . 13 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ((𝑤 = 𝑠 ∨ (𝑠𝑤𝑤𝑠)) → 𝑤𝑠))
5938, 58syl5bi 243 . . . . . . . . . . . 12 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ((𝑤𝑠𝑤 = 𝑠𝑠𝑤) → 𝑤𝑠))
6035, 59syl5 34 . . . . . . . . . . 11 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → ((∀𝑧((𝑧𝑤 ∧ Tr 𝑧) → 𝑧𝑤) ∧ ∀𝑡((𝑡𝑠 ∧ Tr 𝑡) → 𝑡𝑠)) → 𝑤𝑠))
6114, 32, 60mp2and 695 . . . . . . . . . 10 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) ∧ 𝑤𝑦) → 𝑤𝑠)
6261ex 413 . . . . . . . . 9 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (𝑤𝑦𝑤𝑠))
6362ssrdv 3970 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → 𝑦𝑠)
64 dfpss2 4059 . . . . . . . . 9 (𝑦𝑠 ↔ (𝑦𝑠 ∧ ¬ 𝑦 = 𝑠))
65 psseq1 4061 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → (𝑧𝑠𝑦𝑠))
66 treq 5169 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → (Tr 𝑧 ↔ Tr 𝑦))
6765, 66anbi12d 630 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → ((𝑧𝑠 ∧ Tr 𝑧) ↔ (𝑦𝑠 ∧ Tr 𝑦)))
68 elequ1 2112 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → (𝑧𝑠𝑦𝑠))
6967, 68imbi12d 346 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦 → (((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) ↔ ((𝑦𝑠 ∧ Tr 𝑦) → 𝑦𝑠)))
7069spvv 1994 . . . . . . . . . . . . . . . 16 (∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) → ((𝑦𝑠 ∧ Tr 𝑦) → 𝑦𝑠))
7170expd 416 . . . . . . . . . . . . . . 15 (∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) → (𝑦𝑠 → (Tr 𝑦𝑦𝑠)))
7271com23 86 . . . . . . . . . . . . . 14 (∀𝑧((𝑧𝑠 ∧ Tr 𝑧) → 𝑧𝑠) → (Tr 𝑦 → (𝑦𝑠𝑦𝑠)))
7322, 72syl6 35 . . . . . . . . . . . . 13 (𝑠 ∈ (𝑆𝑦) → (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → (Tr 𝑦 → (𝑦𝑠𝑦𝑠))))
7473com3l 89 . . . . . . . . . . . 12 (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → (Tr 𝑦 → (𝑠 ∈ (𝑆𝑦) → (𝑦𝑠𝑦𝑠))))
7574adantld 491 . . . . . . . . . . 11 (∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥) → ((𝑦𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆𝑦) → (𝑦𝑠𝑦𝑠))))
7675adantl 482 . . . . . . . . . 10 ((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) → ((𝑦𝑆 ∧ Tr 𝑦) → (𝑠 ∈ (𝑆𝑦) → (𝑦𝑠𝑦𝑠))))
7776imp32 419 . . . . . . . . 9 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (𝑦𝑠𝑦𝑠))
7864, 77syl5bir 244 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → ((𝑦𝑠 ∧ ¬ 𝑦 = 𝑠) → 𝑦𝑠))
7963, 78mpand 691 . . . . . . 7 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (¬ 𝑦 = 𝑠𝑦𝑠))
8079orrd 857 . . . . . 6 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ ((𝑦𝑆 ∧ Tr 𝑦) ∧ 𝑠 ∈ (𝑆𝑦))) → (𝑦 = 𝑠𝑦𝑠))
8180anassrs 468 . . . . 5 ((((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) ∧ 𝑠 ∈ (𝑆𝑦)) → (𝑦 = 𝑠𝑦𝑠))
8281ralrimiva 3179 . . . 4 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → ∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠))
83 pssdif 4323 . . . . . . 7 (𝑦𝑆 → (𝑆𝑦) ≠ ∅)
84 r19.2z 4436 . . . . . . . 8 (((𝑆𝑦) ≠ ∅ ∧ ∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠))
8584ex 413 . . . . . . 7 ((𝑆𝑦) ≠ ∅ → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
8683, 85syl 17 . . . . . 6 (𝑦𝑆 → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
8786ad2antrl 724 . . . . 5 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → ∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠)))
88 eleq1w 2892 . . . . . . . . . 10 (𝑦 = 𝑠 → (𝑦𝑆𝑠𝑆))
8915, 88syl5ibr 247 . . . . . . . . 9 (𝑦 = 𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆))
9089a1i 11 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (𝑦 = 𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
91 trel 5170 . . . . . . . . . . 11 (Tr 𝑆 → ((𝑦𝑠𝑠𝑆) → 𝑦𝑆))
9291expd 416 . . . . . . . . . 10 (Tr 𝑆 → (𝑦𝑠 → (𝑠𝑆𝑦𝑆)))
9315, 92syl7 74 . . . . . . . . 9 (Tr 𝑆 → (𝑦𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
9493ad2antrr 722 . . . . . . . 8 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (𝑦𝑠 → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
9590, 94jaod 853 . . . . . . 7 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → ((𝑦 = 𝑠𝑦𝑠) → (𝑠 ∈ (𝑆𝑦) → 𝑦𝑆)))
9695com23 86 . . . . . 6 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (𝑠 ∈ (𝑆𝑦) → ((𝑦 = 𝑠𝑦𝑠) → 𝑦𝑆)))
9796rexlimdv 3280 . . . . 5 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (∃𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → 𝑦𝑆))
9887, 97syld 47 . . . 4 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → (∀𝑠 ∈ (𝑆𝑦)(𝑦 = 𝑠𝑦𝑠) → 𝑦𝑆))
9982, 98mpd 15 . . 3 (((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) ∧ (𝑦𝑆 ∧ Tr 𝑦)) → 𝑦𝑆)
10099ex 413 . 2 ((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) → ((𝑦𝑆 ∧ Tr 𝑦) → 𝑦𝑆))
101100alrimiv 1919 1 ((Tr 𝑆 ∧ ∀𝑥𝑆𝑧((𝑧𝑥 ∧ Tr 𝑧) → 𝑧𝑥)) → ∀𝑦((𝑦𝑆 ∧ Tr 𝑦) → 𝑦𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 841  w3o 1078  wal 1526  wcel 2105  wne 3013  wral 3135  wrex 3136  cdif 3930  wss 3933  wpss 3934  c0 4288  Tr wtr 5163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-pw 4537  df-sn 4558  df-pr 4560  df-uni 4831  df-iun 4912  df-tr 5164  df-suc 6190
This theorem is referenced by:  dfon2lem7  32931  dfon2lem8  32932
  Copyright terms: Public domain W3C validator