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

Theorem dfon2lem7 31668
 Description: Lemma for dfon2 31671. 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 1995 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑧 → (𝑡𝑡𝑧𝑡))
2 elequ2 2002 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑧 → (𝑧𝑡𝑧𝑧))
31, 2bitrd 268 . . . . . . . . . . . . . . 15 (𝑡 = 𝑧 → (𝑡𝑡𝑧𝑧))
43notbid 308 . . . . . . . . . . . . . 14 (𝑡 = 𝑧 → (¬ 𝑡𝑡 ↔ ¬ 𝑧𝑧))
54cbvralv 3166 . . . . . . . . . . . . 13 (∀𝑡𝑥 ¬ 𝑡𝑡 ↔ ∀𝑧𝑥 ¬ 𝑧𝑧)
65biimpi 206 . . . . . . . . . . . 12 (∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑧𝑥 ¬ 𝑧𝑧)
76ralimi 2949 . . . . . . . . . . 11 (∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧𝑥 ¬ 𝑧𝑧)
8 untuni 31560 . . . . . . . . . . 11 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 ↔ ∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧𝑥 ¬ 𝑧𝑧)
97, 8sylibr 224 . . . . . . . . . 10 (∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧)
10 vex 3198 . . . . . . . . . . . 12 𝑥 ∈ V
11 sseq1 3618 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑤𝐴𝑥𝐴))
12 treq 4749 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (Tr 𝑤 ↔ Tr 𝑥))
13 raleq 3133 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
1411, 12, 133anbi123d 1397 . . . . . . . . . . . 12 (𝑤 = 𝑥 → ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))))
1510, 14elab 3344 . . . . . . . . . . 11 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
16 vex 3198 . . . . . . . . . . . . . . . 16 𝑡 ∈ V
17 dfon2lem3 31664 . . . . . . . . . . . . . . . 16 (𝑡 ∈ V → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝑡 ∧ ∀𝑢𝑡 ¬ 𝑢𝑢)))
1816, 17ax-mp 5 . . . . . . . . . . . . . . 15 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝑡 ∧ ∀𝑢𝑡 ¬ 𝑢𝑢))
1918simprd 479 . . . . . . . . . . . . . 14 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ∀𝑢𝑡 ¬ 𝑢𝑢)
20 untelirr 31559 . . . . . . . . . . . . . 14 (∀𝑢𝑡 ¬ 𝑢𝑢 → ¬ 𝑡𝑡)
2119, 20syl 17 . . . . . . . . . . . . 13 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ¬ 𝑡𝑡)
2221ralimi 2949 . . . . . . . . . . . 12 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ∀𝑡𝑥 ¬ 𝑡𝑡)
23223ad2ant3 1082 . . . . . . . . . . 11 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → ∀𝑡𝑥 ¬ 𝑡𝑡)
2415, 23sylbi 207 . . . . . . . . . 10 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑡𝑥 ¬ 𝑡𝑡)
259, 24mprg 2923 . . . . . . . . 9 𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧
26 untelirr 31559 . . . . . . . . . 10 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
27 psseq2 3687 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑢 → (𝑦𝑡𝑦𝑢))
2827anbi1d 740 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑢 → ((𝑦𝑡 ∧ Tr 𝑦) ↔ (𝑦𝑢 ∧ Tr 𝑦)))
29 elequ2 2002 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑢 → (𝑦𝑡𝑦𝑢))
3028, 29imbi12d 334 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑢 → (((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3130albidv 1847 . . . . . . . . . . . . . . 15 (𝑡 = 𝑢 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3231cbvralv 3166 . . . . . . . . . . . . . 14 (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
33323anbi3i 1253 . . . . . . . . . . . . 13 ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3433abbii 2737 . . . . . . . . . . . 12 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
3534unieqi 4436 . . . . . . . . . . 11 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
3635eleq2i 2691 . . . . . . . . . 10 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
3726, 36sylnib 318 . . . . . . . . 9 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
3825, 37ax-mp 5 . . . . . . . 8 ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
39 dfon2lem7.1 . . . . . . . . . 10 𝐴 ∈ V
40 dfon2lem2 31663 . . . . . . . . . 10 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴
4139, 40ssexi 4794 . . . . . . . . 9 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ V
4241snss 4307 . . . . . . . 8 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ↔ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
4338, 42mtbi 312 . . . . . . 7 ¬ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
4443intnan 959 . . . . . 6 ¬ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
45 df-suc 5717 . . . . . . . 8 suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}})
4645sseq1i 3621 . . . . . . 7 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
47 unss 3779 . . . . . . 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 313 . . . . 5 ¬ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
5041snss 4307 . . . . . 6 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴 ↔ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴)
5145sseq1i 3621 . . . . . . . . 9 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ 𝐴)
52 unss 3779 . . . . . . . . 9 (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴) ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ 𝐴)
5351, 52bitr4i 267 . . . . . . . 8 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴))
54 dfon2lem1 31662 . . . . . . . . . . . 12 Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}
55 suctr 5796 . . . . . . . . . . . 12 (Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
5654, 55ax-mp 5 . . . . . . . . . . 11 Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}
57 vex 3198 . . . . . . . . . . . . . 14 𝑢 ∈ V
5857elsuc 5782 . . . . . . . . . . . . 13 (𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∨ 𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
59 eluni2 4431 . . . . . . . . . . . . . . 15 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ ∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥)
60 nfa1 2026 . . . . . . . . . . . . . . . 16 𝑥𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)
6131rspccv 3301 . . . . . . . . . . . . . . . . . . 19 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
62 psseq1 3686 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑥 → (𝑦𝑢𝑥𝑢))
63 treq 4749 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑥 → (Tr 𝑦 ↔ Tr 𝑥))
6462, 63anbi12d 746 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → ((𝑦𝑢 ∧ Tr 𝑦) ↔ (𝑥𝑢 ∧ Tr 𝑥)))
65 elequ1 1995 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → (𝑦𝑢𝑥𝑢))
6664, 65imbi12d 334 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → (((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
6766cbvalv 2271 . . . . . . . . . . . . . . . . . . 19 (∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
6861, 67syl6ib 241 . . . . . . . . . . . . . . . . . 18 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
69683ad2ant3 1082 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
7015, 69sylbi 207 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
7160, 70rexlimi 3020 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
7259, 71sylbi 207 . . . . . . . . . . . . . 14 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
73 psseq1 3686 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑦𝑢𝑧𝑢))
74 treq 4749 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (Tr 𝑦 ↔ Tr 𝑧))
7573, 74anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → ((𝑦𝑢 ∧ Tr 𝑦) ↔ (𝑧𝑢 ∧ Tr 𝑧)))
76 elequ1 1995 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → (𝑦𝑢𝑧𝑢))
7775, 76imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑧 → (((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
7877cbvalv 2271 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
7961, 78syl6ib 241 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
80793ad2ant3 1082 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
8115, 80sylbi 207 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
8281rexlimiv 3023 . . . . . . . . . . . . . . . . . 18 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
8359, 82sylbi 207 . . . . . . . . . . . . . . . . 17 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
8483rgen 2919 . . . . . . . . . . . . . . . 16 𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)
85 dfon2lem6 31667 . . . . . . . . . . . . . . . 16 ((Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)) → ∀𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
8654, 84, 85mp2an 707 . . . . . . . . . . . . . . 15 𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
87 psseq2 3687 . . . . . . . . . . . . . . . . . 18 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝑢𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
8887anbi1d 740 . . . . . . . . . . . . . . . . 17 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑥𝑢 ∧ Tr 𝑥) ↔ (𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥)))
89 eleq2 2688 . . . . . . . . . . . . . . . . 17 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝑢𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
9088, 89imbi12d 334 . . . . . . . . . . . . . . . 16 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
9190albidv 1847 . . . . . . . . . . . . . . 15 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
9286, 91mpbiri 248 . . . . . . . . . . . . . 14 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9372, 92jaoi 394 . . . . . . . . . . . . 13 ((𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∨ 𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9458, 93sylbi 207 . . . . . . . . . . . 12 (𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9594rgen 2919 . . . . . . . . . . 11 𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)
9641sucex 6996 . . . . . . . . . . . . 13 suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ V
97 sseq1 3618 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑠𝐴 ↔ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴))
98 treq 4749 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (Tr 𝑠 ↔ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
99 raleq 3133 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
10097, 98, 993anbi123d 1397 . . . . . . . . . . . . 13 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)) ↔ (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))))
10196, 100elab 3344 . . . . . . . . . . . 12 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} ↔ (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
102 elssuni 4458 . . . . . . . . . . . 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 1414 . . . . . . . . . 10 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))})
105 sseq1 3618 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (𝑠𝐴𝑤𝐴))
106 treq 4749 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (Tr 𝑠 ↔ Tr 𝑤))
107 raleq 3133 . . . . . . . . . . . . . 14 (𝑠 = 𝑤 → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
108 psseq1 3686 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑥𝑢𝑦𝑢))
109 treq 4749 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (Tr 𝑥 ↔ Tr 𝑦))
110108, 109anbi12d 746 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝑥𝑢 ∧ Tr 𝑥) ↔ (𝑦𝑢 ∧ Tr 𝑦)))
111 elequ1 1995 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑥𝑢𝑦𝑢))
112110, 111imbi12d 334 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
113112cbvalv 2271 . . . . . . . . . . . . . . 15 (∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
114113ralbii 2977 . . . . . . . . . . . . . 14 (∀𝑢𝑤𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
115107, 114syl6bb 276 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
116105, 106, 1153anbi123d 1397 . . . . . . . . . . . 12 (𝑠 = 𝑤 → ((𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)) ↔ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))))
117116cbvabv 2745 . . . . . . . . . . 11 {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
118117unieqi 4436 . . . . . . . . . 10 {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
119104, 118syl6sseq 3643 . . . . . . . . 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 711 . . . . . 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 3686 . . . . . . . 8 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴))
126 treq 4749 . . . . . . . 8 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (Tr 𝑥 ↔ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
127125, 126anbi12d 746 . . . . . . 7 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑥𝐴 ∧ Tr 𝑥) ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
128 eleq1 2687 . . . . . . 7 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
129127, 128imbi12d 334 . . . . . 6 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) ↔ (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴)))
13041, 129spcv 3294 . . . . 5 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
13154, 130mpan2i 712 . . . 4 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
132124, 131mtod 189 . . 3 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
133 dfpss2 3684 . . . . 5 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴))
134133biimpri 218 . . . 4 (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
13540, 134mpan 705 . . 3 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
136132, 135nsyl2 142 . 2 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴)
137 eluni2 4431 . . . . 5 (𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ ∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑧𝑥)
138 psseq2 3687 . . . . . . . . . . . . . 14 (𝑡 = 𝑧 → (𝑦𝑡𝑦𝑧))
139138anbi1d 740 . . . . . . . . . . . . 13 (𝑡 = 𝑧 → ((𝑦𝑡 ∧ Tr 𝑦) ↔ (𝑦𝑧 ∧ Tr 𝑦)))
140 elequ2 2002 . . . . . . . . . . . . 13 (𝑡 = 𝑧 → (𝑦𝑡𝑦𝑧))
141139, 140imbi12d 334 . . . . . . . . . . . 12 (𝑡 = 𝑧 → (((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
142141albidv 1847 . . . . . . . . . . 11 (𝑡 = 𝑧 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
143142cbvralv 3166 . . . . . . . . . 10 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
14413, 143syl6bb 276 . . . . . . . . 9 (𝑤 = 𝑥 → (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
14511, 12, 1443anbi123d 1397 . . . . . . . 8 (𝑤 = 𝑥 → ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))))
14610, 145elab 3344 . . . . . . 7 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
147 rsp 2926 . . . . . . . 8 (∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
1481473ad2ant3 1082 . . . . . . 7 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)) → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
149146, 148sylbi 207 . . . . . 6 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
150149rexlimiv 3023 . . . . 5 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
151137, 150sylbi 207 . . . 4 (𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
152151rgen 2919 . . 3 𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)
153 raleq 3133 . . 3 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 → (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
154152, 153mpbii 223 . 2 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 → ∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
155 psseq2 3687 . . . . . 6 (𝑧 = 𝐵 → (𝑦𝑧𝑦𝐵))
156155anbi1d 740 . . . . 5 (𝑧 = 𝐵 → ((𝑦𝑧 ∧ Tr 𝑦) ↔ (𝑦𝐵 ∧ Tr 𝑦)))
157 eleq2 2688 . . . . 5 (𝑧 = 𝐵 → (𝑦𝑧𝑦𝐵))
158156, 157imbi12d 334 . . . 4 (𝑧 = 𝐵 → (((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
159158albidv 1847 . . 3 (𝑧 = 𝐵 → (∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
160159rspccv 3301 . 2 (∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) → (𝐵𝐴 → ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
161136, 154, 1603syl 18 1 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (𝐵𝐴 → ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 383   ∧ wa 384   ∧ w3a 1036  ∀wal 1479   = wceq 1481   ∈ wcel 1988  {cab 2606  ∀wral 2909  ∃wrex 2910  Vcvv 3195   ∪ cun 3565   ⊆ wss 3567   ⊊ wpss 3568  {csn 4168  ∪ cuni 4427  Tr wtr 4743  suc csuc 5713 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897  ax-un 6934 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-pw 4151  df-sn 4169  df-pr 4171  df-uni 4428  df-iun 4513  df-tr 4744  df-suc 5717 This theorem is referenced by:  dfon2lem8  31669  dfon2  31671
 Copyright terms: Public domain W3C validator