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

Theorem dfon2lem7 35294
Description: Lemma for dfon2 35297. All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011.)
Hypothesis
Ref Expression
dfon2lem7.1 𝐴 ∈ V
Assertion
Ref Expression
dfon2lem7 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (𝐵𝐴 → ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Proof of Theorem dfon2lem7
Dummy variables 𝑧 𝑤 𝑠 𝑡 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elequ1 2105 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑧 → (𝑡𝑡𝑧𝑡))
2 elequ2 2113 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑧 → (𝑧𝑡𝑧𝑧))
31, 2bitrd 279 . . . . . . . . . . . . . . 15 (𝑡 = 𝑧 → (𝑡𝑡𝑧𝑧))
43notbid 318 . . . . . . . . . . . . . 14 (𝑡 = 𝑧 → (¬ 𝑡𝑡 ↔ ¬ 𝑧𝑧))
54cbvralvw 3228 . . . . . . . . . . . . 13 (∀𝑡𝑥 ¬ 𝑡𝑡 ↔ ∀𝑧𝑥 ¬ 𝑧𝑧)
65biimpi 215 . . . . . . . . . . . 12 (∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑧𝑥 ¬ 𝑧𝑧)
76ralimi 3077 . . . . . . . . . . 11 (∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧𝑥 ¬ 𝑧𝑧)
8 untuni 35212 . . . . . . . . . . 11 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 ↔ ∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧𝑥 ¬ 𝑧𝑧)
97, 8sylibr 233 . . . . . . . . . 10 (∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧)
10 vex 3472 . . . . . . . . . . . 12 𝑥 ∈ V
11 sseq1 4002 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑤𝐴𝑥𝐴))
12 treq 5266 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (Tr 𝑤 ↔ Tr 𝑥))
13 raleq 3316 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
1411, 12, 133anbi123d 1432 . . . . . . . . . . . 12 (𝑤 = 𝑥 → ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))))
1510, 14elab 3663 . . . . . . . . . . 11 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
16 vex 3472 . . . . . . . . . . . . . . . 16 𝑡 ∈ V
17 dfon2lem3 35290 . . . . . . . . . . . . . . . 16 (𝑡 ∈ V → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝑡 ∧ ∀𝑢𝑡 ¬ 𝑢𝑢)))
1816, 17ax-mp 5 . . . . . . . . . . . . . . 15 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝑡 ∧ ∀𝑢𝑡 ¬ 𝑢𝑢))
1918simprd 495 . . . . . . . . . . . . . 14 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ∀𝑢𝑡 ¬ 𝑢𝑢)
20 untelirr 35211 . . . . . . . . . . . . . 14 (∀𝑢𝑡 ¬ 𝑢𝑢 → ¬ 𝑡𝑡)
2119, 20syl 17 . . . . . . . . . . . . 13 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ¬ 𝑡𝑡)
2221ralimi 3077 . . . . . . . . . . . 12 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ∀𝑡𝑥 ¬ 𝑡𝑡)
23223ad2ant3 1132 . . . . . . . . . . 11 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → ∀𝑡𝑥 ¬ 𝑡𝑡)
2415, 23sylbi 216 . . . . . . . . . 10 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑡𝑥 ¬ 𝑡𝑡)
259, 24mprg 3061 . . . . . . . . 9 𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧
26 untelirr 35211 . . . . . . . . . 10 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
27 psseq2 4083 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑢 → (𝑦𝑡𝑦𝑢))
2827anbi1d 629 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑢 → ((𝑦𝑡 ∧ Tr 𝑦) ↔ (𝑦𝑢 ∧ Tr 𝑦)))
29 elequ2 2113 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑢 → (𝑦𝑡𝑦𝑢))
3028, 29imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑢 → (((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3130albidv 1915 . . . . . . . . . . . . . . 15 (𝑡 = 𝑢 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3231cbvralvw 3228 . . . . . . . . . . . . . 14 (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
33323anbi3i 1156 . . . . . . . . . . . . 13 ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3433abbii 2796 . . . . . . . . . . . 12 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
3534unieqi 4914 . . . . . . . . . . 11 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
3635eleq2i 2819 . . . . . . . . . 10 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
3726, 36sylnib 328 . . . . . . . . 9 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
3825, 37ax-mp 5 . . . . . . . 8 ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
39 dfon2lem7.1 . . . . . . . . . 10 𝐴 ∈ V
40 dfon2lem2 35289 . . . . . . . . . 10 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴
4139, 40ssexi 5315 . . . . . . . . 9 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ V
4241snss 4784 . . . . . . . 8 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ↔ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
4338, 42mtbi 322 . . . . . . 7 ¬ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
4443intnan 486 . . . . . 6 ¬ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
45 df-suc 6364 . . . . . . . 8 suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}})
4645sseq1i 4005 . . . . . . 7 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
47 unss 4179 . . . . . . 7 (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}) ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
4846, 47bitr4i 278 . . . . . 6 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
4944, 48mtbir 323 . . . . 5 ¬ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
5041snss 4784 . . . . . 6 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴 ↔ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴)
5145sseq1i 4005 . . . . . . . . 9 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ 𝐴)
52 unss 4179 . . . . . . . . 9 (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴) ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ 𝐴)
5351, 52bitr4i 278 . . . . . . . 8 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴))
54 dfon2lem1 35288 . . . . . . . . . . . 12 Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}
55 suctr 6444 . . . . . . . . . . . 12 (Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
5654, 55ax-mp 5 . . . . . . . . . . 11 Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}
57 vex 3472 . . . . . . . . . . . . . 14 𝑢 ∈ V
5857elsuc 6428 . . . . . . . . . . . . 13 (𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∨ 𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
59 eluni2 4906 . . . . . . . . . . . . . . 15 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ ∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥)
60 nfa1 2140 . . . . . . . . . . . . . . . 16 𝑥𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)
6131rspccv 3603 . . . . . . . . . . . . . . . . . . 19 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
62 psseq1 4082 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑥 → (𝑦𝑢𝑥𝑢))
63 treq 5266 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑥 → (Tr 𝑦 ↔ Tr 𝑥))
6462, 63anbi12d 630 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → ((𝑦𝑢 ∧ Tr 𝑦) ↔ (𝑥𝑢 ∧ Tr 𝑥)))
65 elequ1 2105 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → (𝑦𝑢𝑥𝑢))
6664, 65imbi12d 344 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → (((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
6766cbvalvw 2031 . . . . . . . . . . . . . . . . . . 19 (∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
6861, 67imbitrdi 250 . . . . . . . . . . . . . . . . . 18 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
69683ad2ant3 1132 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
7015, 69sylbi 216 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
7160, 70rexlimi 3250 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
7259, 71sylbi 216 . . . . . . . . . . . . . 14 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
73 psseq1 4082 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑦𝑢𝑧𝑢))
74 treq 5266 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (Tr 𝑦 ↔ Tr 𝑧))
7573, 74anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → ((𝑦𝑢 ∧ Tr 𝑦) ↔ (𝑧𝑢 ∧ Tr 𝑧)))
76 elequ1 2105 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → (𝑦𝑢𝑧𝑢))
7775, 76imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑧 → (((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
7877cbvalvw 2031 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
7961, 78imbitrdi 250 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
80793ad2ant3 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
8115, 80sylbi 216 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
8281rexlimiv 3142 . . . . . . . . . . . . . . . . . 18 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
8359, 82sylbi 216 . . . . . . . . . . . . . . . . 17 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
8483rgen 3057 . . . . . . . . . . . . . . . 16 𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)
85 dfon2lem6 35293 . . . . . . . . . . . . . . . 16 ((Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)) → ∀𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
8654, 84, 85mp2an 689 . . . . . . . . . . . . . . 15 𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
87 psseq2 4083 . . . . . . . . . . . . . . . . . 18 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝑢𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
8887anbi1d 629 . . . . . . . . . . . . . . . . 17 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑥𝑢 ∧ Tr 𝑥) ↔ (𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥)))
89 eleq2 2816 . . . . . . . . . . . . . . . . 17 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝑢𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
9088, 89imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
9190albidv 1915 . . . . . . . . . . . . . . 15 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
9286, 91mpbiri 258 . . . . . . . . . . . . . 14 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9372, 92jaoi 854 . . . . . . . . . . . . 13 ((𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∨ 𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9458, 93sylbi 216 . . . . . . . . . . . 12 (𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9594rgen 3057 . . . . . . . . . . 11 𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)
9641sucex 7791 . . . . . . . . . . . . 13 suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ V
97 sseq1 4002 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑠𝐴 ↔ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴))
98 treq 5266 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (Tr 𝑠 ↔ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
99 raleq 3316 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
10097, 98, 993anbi123d 1432 . . . . . . . . . . . . 13 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)) ↔ (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))))
10196, 100elab 3663 . . . . . . . . . . . 12 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} ↔ (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
102 elssuni 4934 . . . . . . . . . . . 12 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))})
103101, 102sylbir 234 . . . . . . . . . . 11 ((suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)) → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))})
10456, 95, 103mp3an23 1449 . . . . . . . . . 10 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))})
105 sseq1 4002 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (𝑠𝐴𝑤𝐴))
106 treq 5266 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (Tr 𝑠 ↔ Tr 𝑤))
107 raleq 3316 . . . . . . . . . . . . . 14 (𝑠 = 𝑤 → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
108 psseq1 4082 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑥𝑢𝑦𝑢))
109 treq 5266 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (Tr 𝑥 ↔ Tr 𝑦))
110108, 109anbi12d 630 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝑥𝑢 ∧ Tr 𝑥) ↔ (𝑦𝑢 ∧ Tr 𝑦)))
111 elequ1 2105 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑥𝑢𝑦𝑢))
112110, 111imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
113112cbvalvw 2031 . . . . . . . . . . . . . . 15 (∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
114113ralbii 3087 . . . . . . . . . . . . . 14 (∀𝑢𝑤𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
115107, 114bitrdi 287 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
116105, 106, 1153anbi123d 1432 . . . . . . . . . . . 12 (𝑠 = 𝑤 → ((𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)) ↔ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))))
117116cbvabv 2799 . . . . . . . . . . 11 {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
118117unieqi 4914 . . . . . . . . . 10 {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
119104, 118sseqtrdi 4027 . . . . . . . . 9 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
120119a1i 11 . . . . . . . 8 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12153, 120biimtrrid 242 . . . . . . 7 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴) → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12240, 121mpani 693 . . . . . 6 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ({ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12350, 122biimtrid 241 . . . . 5 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12449, 123mtoi 198 . . . 4 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴)
125 psseq1 4082 . . . . . . . 8 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴))
126 treq 5266 . . . . . . . 8 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (Tr 𝑥 ↔ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
127125, 126anbi12d 630 . . . . . . 7 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑥𝐴 ∧ Tr 𝑥) ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
128 eleq1 2815 . . . . . . 7 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
129127, 128imbi12d 344 . . . . . 6 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) ↔ (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴)))
13041, 129spcv 3589 . . . . 5 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
13154, 130mpan2i 694 . . . 4 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
132124, 131mtod 197 . . 3 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
133 dfpss2 4080 . . . . 5 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴))
134133biimpri 227 . . . 4 (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
13540, 134mpan 687 . . 3 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
136132, 135nsyl2 141 . 2 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴)
137 eluni2 4906 . . . . 5 (𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ ∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑧𝑥)
138 psseq2 4083 . . . . . . . . . . . . . 14 (𝑡 = 𝑧 → (𝑦𝑡𝑦𝑧))
139138anbi1d 629 . . . . . . . . . . . . 13 (𝑡 = 𝑧 → ((𝑦𝑡 ∧ Tr 𝑦) ↔ (𝑦𝑧 ∧ Tr 𝑦)))
140 elequ2 2113 . . . . . . . . . . . . 13 (𝑡 = 𝑧 → (𝑦𝑡𝑦𝑧))
141139, 140imbi12d 344 . . . . . . . . . . . 12 (𝑡 = 𝑧 → (((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
142141albidv 1915 . . . . . . . . . . 11 (𝑡 = 𝑧 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
143142cbvralvw 3228 . . . . . . . . . 10 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
14413, 143bitrdi 287 . . . . . . . . 9 (𝑤 = 𝑥 → (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
14511, 12, 1443anbi123d 1432 . . . . . . . 8 (𝑤 = 𝑥 → ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))))
14610, 145elab 3663 . . . . . . 7 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
147 rsp 3238 . . . . . . . 8 (∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
1481473ad2ant3 1132 . . . . . . 7 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)) → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
149146, 148sylbi 216 . . . . . 6 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
150149rexlimiv 3142 . . . . 5 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
151137, 150sylbi 216 . . . 4 (𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
152151rgen 3057 . . 3 𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)
153 raleq 3316 . . 3 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 → (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
154152, 153mpbii 232 . 2 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 → ∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
155 psseq2 4083 . . . . . 6 (𝑧 = 𝐵 → (𝑦𝑧𝑦𝐵))
156155anbi1d 629 . . . . 5 (𝑧 = 𝐵 → ((𝑦𝑧 ∧ Tr 𝑦) ↔ (𝑦𝐵 ∧ Tr 𝑦)))
157 eleq2 2816 . . . . 5 (𝑧 = 𝐵 → (𝑦𝑧𝑦𝐵))
158156, 157imbi12d 344 . . . 4 (𝑧 = 𝐵 → (((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
159158albidv 1915 . . 3 (𝑧 = 𝐵 → (∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
160159rspccv 3603 . 2 (∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) → (𝐵𝐴 → ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
161136, 154, 1603syl 18 1 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (𝐵𝐴 → ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 844  w3a 1084  wal 1531   = wceq 1533  wcel 2098  {cab 2703  wral 3055  wrex 3064  Vcvv 3468  cun 3941  wss 3943  wpss 3944  {csn 4623   cuni 4902  Tr wtr 5258  suc csuc 6360
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-sbc 3773  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-pw 4599  df-sn 4624  df-pr 4626  df-uni 4903  df-iun 4992  df-tr 5259  df-suc 6364
This theorem is referenced by:  dfon2lem8  35295  dfon2  35297
  Copyright terms: Public domain W3C validator