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 31818
Description: Lemma for dfon2 31821. 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 2037 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑧 → (𝑡𝑡𝑧𝑡))
2 elequ2 2044 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑧 → (𝑧𝑡𝑧𝑧))
31, 2bitrd 268 . . . . . . . . . . . . . . 15 (𝑡 = 𝑧 → (𝑡𝑡𝑧𝑧))
43notbid 307 . . . . . . . . . . . . . 14 (𝑡 = 𝑧 → (¬ 𝑡𝑡 ↔ ¬ 𝑧𝑧))
54cbvralv 3201 . . . . . . . . . . . . 13 (∀𝑡𝑥 ¬ 𝑡𝑡 ↔ ∀𝑧𝑥 ¬ 𝑧𝑧)
65biimpi 206 . . . . . . . . . . . 12 (∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑧𝑥 ¬ 𝑧𝑧)
76ralimi 2981 . . . . . . . . . . 11 (∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧𝑥 ¬ 𝑧𝑧)
8 untuni 31712 . . . . . . . . . . 11 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 ↔ ∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧𝑥 ¬ 𝑧𝑧)
97, 8sylibr 224 . . . . . . . . . 10 (∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧)
10 vex 3234 . . . . . . . . . . . 12 𝑥 ∈ V
11 sseq1 3659 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑤𝐴𝑥𝐴))
12 treq 4791 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (Tr 𝑤 ↔ Tr 𝑥))
13 raleq 3168 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
1411, 12, 133anbi123d 1439 . . . . . . . . . . . 12 (𝑤 = 𝑥 → ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))))
1510, 14elab 3382 . . . . . . . . . . 11 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
16 vex 3234 . . . . . . . . . . . . . . . 16 𝑡 ∈ V
17 dfon2lem3 31814 . . . . . . . . . . . . . . . 16 (𝑡 ∈ V → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝑡 ∧ ∀𝑢𝑡 ¬ 𝑢𝑢)))
1816, 17ax-mp 5 . . . . . . . . . . . . . . 15 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝑡 ∧ ∀𝑢𝑡 ¬ 𝑢𝑢))
1918simprd 478 . . . . . . . . . . . . . 14 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ∀𝑢𝑡 ¬ 𝑢𝑢)
20 untelirr 31711 . . . . . . . . . . . . . 14 (∀𝑢𝑡 ¬ 𝑢𝑢 → ¬ 𝑡𝑡)
2119, 20syl 17 . . . . . . . . . . . . 13 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ¬ 𝑡𝑡)
2221ralimi 2981 . . . . . . . . . . . 12 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ∀𝑡𝑥 ¬ 𝑡𝑡)
23223ad2ant3 1104 . . . . . . . . . . 11 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → ∀𝑡𝑥 ¬ 𝑡𝑡)
2415, 23sylbi 207 . . . . . . . . . 10 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑡𝑥 ¬ 𝑡𝑡)
259, 24mprg 2955 . . . . . . . . 9 𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧
26 untelirr 31711 . . . . . . . . . 10 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
27 psseq2 3728 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑢 → (𝑦𝑡𝑦𝑢))
2827anbi1d 741 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑢 → ((𝑦𝑡 ∧ Tr 𝑦) ↔ (𝑦𝑢 ∧ Tr 𝑦)))
29 elequ2 2044 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑢 → (𝑦𝑡𝑦𝑢))
3028, 29imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑢 → (((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3130albidv 1889 . . . . . . . . . . . . . . 15 (𝑡 = 𝑢 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3231cbvralv 3201 . . . . . . . . . . . . . 14 (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
33323anbi3i 1274 . . . . . . . . . . . . 13 ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3433abbii 2768 . . . . . . . . . . . 12 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
3534unieqi 4477 . . . . . . . . . . 11 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
3635eleq2i 2722 . . . . . . . . . 10 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
3726, 36sylnib 317 . . . . . . . . 9 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
3825, 37ax-mp 5 . . . . . . . 8 ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
39 dfon2lem7.1 . . . . . . . . . 10 𝐴 ∈ V
40 dfon2lem2 31813 . . . . . . . . . 10 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴
4139, 40ssexi 4836 . . . . . . . . 9 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ V
4241snss 4348 . . . . . . . 8 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ↔ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
4338, 42mtbi 311 . . . . . . 7 ¬ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
4443intnan 980 . . . . . 6 ¬ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
45 df-suc 5767 . . . . . . . 8 suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}})
4645sseq1i 3662 . . . . . . 7 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
47 unss 3820 . . . . . . 7 (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}) ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
4846, 47bitr4i 267 . . . . . 6 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
4944, 48mtbir 312 . . . . 5 ¬ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
5041snss 4348 . . . . . 6 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴 ↔ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴)
5145sseq1i 3662 . . . . . . . . 9 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ 𝐴)
52 unss 3820 . . . . . . . . 9 (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴) ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ 𝐴)
5351, 52bitr4i 267 . . . . . . . 8 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴))
54 dfon2lem1 31812 . . . . . . . . . . . 12 Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}
55 suctr 5846 . . . . . . . . . . . 12 (Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
5654, 55ax-mp 5 . . . . . . . . . . 11 Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}
57 vex 3234 . . . . . . . . . . . . . 14 𝑢 ∈ V
5857elsuc 5832 . . . . . . . . . . . . 13 (𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∨ 𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
59 eluni2 4472 . . . . . . . . . . . . . . 15 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ ∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥)
60 nfa1 2068 . . . . . . . . . . . . . . . 16 𝑥𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)
6131rspccv 3337 . . . . . . . . . . . . . . . . . . 19 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
62 psseq1 3727 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑥 → (𝑦𝑢𝑥𝑢))
63 treq 4791 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑥 → (Tr 𝑦 ↔ Tr 𝑥))
6462, 63anbi12d 747 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → ((𝑦𝑢 ∧ Tr 𝑦) ↔ (𝑥𝑢 ∧ Tr 𝑥)))
65 elequ1 2037 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → (𝑦𝑢𝑥𝑢))
6664, 65imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → (((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
6766cbvalv 2309 . . . . . . . . . . . . . . . . . . 19 (∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
6861, 67syl6ib 241 . . . . . . . . . . . . . . . . . 18 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
69683ad2ant3 1104 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
7015, 69sylbi 207 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
7160, 70rexlimi 3053 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
7259, 71sylbi 207 . . . . . . . . . . . . . 14 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
73 psseq1 3727 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑦𝑢𝑧𝑢))
74 treq 4791 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (Tr 𝑦 ↔ Tr 𝑧))
7573, 74anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → ((𝑦𝑢 ∧ Tr 𝑦) ↔ (𝑧𝑢 ∧ Tr 𝑧)))
76 elequ1 2037 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → (𝑦𝑢𝑧𝑢))
7775, 76imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑧 → (((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
7877cbvalv 2309 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
7961, 78syl6ib 241 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
80793ad2ant3 1104 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
8115, 80sylbi 207 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
8281rexlimiv 3056 . . . . . . . . . . . . . . . . . 18 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
8359, 82sylbi 207 . . . . . . . . . . . . . . . . 17 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
8483rgen 2951 . . . . . . . . . . . . . . . 16 𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)
85 dfon2lem6 31817 . . . . . . . . . . . . . . . 16 ((Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)) → ∀𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
8654, 84, 85mp2an 708 . . . . . . . . . . . . . . 15 𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
87 psseq2 3728 . . . . . . . . . . . . . . . . . 18 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝑢𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
8887anbi1d 741 . . . . . . . . . . . . . . . . 17 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑥𝑢 ∧ Tr 𝑥) ↔ (𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥)))
89 eleq2 2719 . . . . . . . . . . . . . . . . 17 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝑢𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
9088, 89imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
9190albidv 1889 . . . . . . . . . . . . . . 15 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
9286, 91mpbiri 248 . . . . . . . . . . . . . 14 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9372, 92jaoi 393 . . . . . . . . . . . . 13 ((𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∨ 𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9458, 93sylbi 207 . . . . . . . . . . . 12 (𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9594rgen 2951 . . . . . . . . . . 11 𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)
9641sucex 7053 . . . . . . . . . . . . 13 suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ V
97 sseq1 3659 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑠𝐴 ↔ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴))
98 treq 4791 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (Tr 𝑠 ↔ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
99 raleq 3168 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
10097, 98, 993anbi123d 1439 . . . . . . . . . . . . 13 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)) ↔ (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))))
10196, 100elab 3382 . . . . . . . . . . . 12 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} ↔ (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
102 elssuni 4499 . . . . . . . . . . . 12 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))})
103101, 102sylbir 225 . . . . . . . . . . 11 ((suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)) → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))})
10456, 95, 103mp3an23 1456 . . . . . . . . . 10 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))})
105 sseq1 3659 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (𝑠𝐴𝑤𝐴))
106 treq 4791 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (Tr 𝑠 ↔ Tr 𝑤))
107 raleq 3168 . . . . . . . . . . . . . 14 (𝑠 = 𝑤 → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
108 psseq1 3727 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑥𝑢𝑦𝑢))
109 treq 4791 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (Tr 𝑥 ↔ Tr 𝑦))
110108, 109anbi12d 747 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝑥𝑢 ∧ Tr 𝑥) ↔ (𝑦𝑢 ∧ Tr 𝑦)))
111 elequ1 2037 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑥𝑢𝑦𝑢))
112110, 111imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
113112cbvalv 2309 . . . . . . . . . . . . . . 15 (∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
114113ralbii 3009 . . . . . . . . . . . . . 14 (∀𝑢𝑤𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
115107, 114syl6bb 276 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
116105, 106, 1153anbi123d 1439 . . . . . . . . . . . 12 (𝑠 = 𝑤 → ((𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)) ↔ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))))
117116cbvabv 2776 . . . . . . . . . . 11 {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
118117unieqi 4477 . . . . . . . . . 10 {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
119104, 118syl6sseq 3684 . . . . . . . . 9 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
120119a1i 11 . . . . . . . 8 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12153, 120syl5bir 233 . . . . . . 7 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴) → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12240, 121mpani 712 . . . . . 6 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ({ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12350, 122syl5bi 232 . . . . 5 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12449, 123mtoi 190 . . . 4 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴)
125 psseq1 3727 . . . . . . . 8 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴))
126 treq 4791 . . . . . . . 8 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (Tr 𝑥 ↔ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
127125, 126anbi12d 747 . . . . . . 7 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑥𝐴 ∧ Tr 𝑥) ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
128 eleq1 2718 . . . . . . 7 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
129127, 128imbi12d 333 . . . . . 6 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) ↔ (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴)))
13041, 129spcv 3330 . . . . 5 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
13154, 130mpan2i 713 . . . 4 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
132124, 131mtod 189 . . 3 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
133 dfpss2 3725 . . . . 5 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴))
134133biimpri 218 . . . 4 (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
13540, 134mpan 706 . . 3 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
136132, 135nsyl2 142 . 2 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴)
137 eluni2 4472 . . . . 5 (𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ ∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑧𝑥)
138 psseq2 3728 . . . . . . . . . . . . . 14 (𝑡 = 𝑧 → (𝑦𝑡𝑦𝑧))
139138anbi1d 741 . . . . . . . . . . . . 13 (𝑡 = 𝑧 → ((𝑦𝑡 ∧ Tr 𝑦) ↔ (𝑦𝑧 ∧ Tr 𝑦)))
140 elequ2 2044 . . . . . . . . . . . . 13 (𝑡 = 𝑧 → (𝑦𝑡𝑦𝑧))
141139, 140imbi12d 333 . . . . . . . . . . . 12 (𝑡 = 𝑧 → (((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
142141albidv 1889 . . . . . . . . . . 11 (𝑡 = 𝑧 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
143142cbvralv 3201 . . . . . . . . . 10 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
14413, 143syl6bb 276 . . . . . . . . 9 (𝑤 = 𝑥 → (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
14511, 12, 1443anbi123d 1439 . . . . . . . 8 (𝑤 = 𝑥 → ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))))
14610, 145elab 3382 . . . . . . 7 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
147 rsp 2958 . . . . . . . 8 (∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
1481473ad2ant3 1104 . . . . . . 7 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)) → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
149146, 148sylbi 207 . . . . . 6 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
150149rexlimiv 3056 . . . . 5 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
151137, 150sylbi 207 . . . 4 (𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
152151rgen 2951 . . 3 𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)
153 raleq 3168 . . 3 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 → (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
154152, 153mpbii 223 . 2 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 → ∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
155 psseq2 3728 . . . . . 6 (𝑧 = 𝐵 → (𝑦𝑧𝑦𝐵))
156155anbi1d 741 . . . . 5 (𝑧 = 𝐵 → ((𝑦𝑧 ∧ Tr 𝑦) ↔ (𝑦𝐵 ∧ Tr 𝑦)))
157 eleq2 2719 . . . . 5 (𝑧 = 𝐵 → (𝑦𝑧𝑦𝐵))
158156, 157imbi12d 333 . . . 4 (𝑧 = 𝐵 → (((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
159158albidv 1889 . . 3 (𝑧 = 𝐵 → (∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
160159rspccv 3337 . 2 (∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) → (𝐵𝐴 → ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
161136, 154, 1603syl 18 1 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (𝐵𝐴 → ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382  wa 383  w3a 1054  wal 1521   = wceq 1523  wcel 2030  {cab 2637  wral 2941  wrex 2942  Vcvv 3231  cun 3605  wss 3607  wpss 3608  {csn 4210   cuni 4468  Tr wtr 4785  suc csuc 5763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-pw 4193  df-sn 4211  df-pr 4213  df-uni 4469  df-iun 4554  df-tr 4786  df-suc 5767
This theorem is referenced by:  dfon2lem8  31819  dfon2  31821
  Copyright terms: Public domain W3C validator