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 32068
Description: Lemma for dfon2 32071. 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 2162 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑧 → (𝑡𝑡𝑧𝑡))
2 elequ2 2169 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑧 → (𝑧𝑡𝑧𝑧))
31, 2bitrd 270 . . . . . . . . . . . . . . 15 (𝑡 = 𝑧 → (𝑡𝑡𝑧𝑧))
43notbid 309 . . . . . . . . . . . . . 14 (𝑡 = 𝑧 → (¬ 𝑡𝑡 ↔ ¬ 𝑧𝑧))
54cbvralv 3318 . . . . . . . . . . . . 13 (∀𝑡𝑥 ¬ 𝑡𝑡 ↔ ∀𝑧𝑥 ¬ 𝑧𝑧)
65biimpi 207 . . . . . . . . . . . 12 (∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑧𝑥 ¬ 𝑧𝑧)
76ralimi 3098 . . . . . . . . . . 11 (∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧𝑥 ¬ 𝑧𝑧)
8 untuni 31963 . . . . . . . . . . 11 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 ↔ ∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧𝑥 ¬ 𝑧𝑧)
97, 8sylibr 225 . . . . . . . . . 10 (∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧)
10 vex 3352 . . . . . . . . . . . 12 𝑥 ∈ V
11 sseq1 3785 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑤𝐴𝑥𝐴))
12 treq 4916 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (Tr 𝑤 ↔ Tr 𝑥))
13 raleq 3285 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
1411, 12, 133anbi123d 1560 . . . . . . . . . . . 12 (𝑤 = 𝑥 → ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))))
1510, 14elab 3503 . . . . . . . . . . 11 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
16 vex 3352 . . . . . . . . . . . . . . . 16 𝑡 ∈ V
17 dfon2lem3 32064 . . . . . . . . . . . . . . . 16 (𝑡 ∈ V → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝑡 ∧ ∀𝑢𝑡 ¬ 𝑢𝑢)))
1816, 17ax-mp 5 . . . . . . . . . . . . . . 15 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝑡 ∧ ∀𝑢𝑡 ¬ 𝑢𝑢))
1918simprd 489 . . . . . . . . . . . . . 14 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ∀𝑢𝑡 ¬ 𝑢𝑢)
20 untelirr 31962 . . . . . . . . . . . . . 14 (∀𝑢𝑡 ¬ 𝑢𝑢 → ¬ 𝑡𝑡)
2119, 20syl 17 . . . . . . . . . . . . 13 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ¬ 𝑡𝑡)
2221ralimi 3098 . . . . . . . . . . . 12 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ∀𝑡𝑥 ¬ 𝑡𝑡)
23223ad2ant3 1165 . . . . . . . . . . 11 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → ∀𝑡𝑥 ¬ 𝑡𝑡)
2415, 23sylbi 208 . . . . . . . . . 10 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑡𝑥 ¬ 𝑡𝑡)
259, 24mprg 3072 . . . . . . . . 9 𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧
26 untelirr 31962 . . . . . . . . . 10 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
27 psseq2 3855 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑢 → (𝑦𝑡𝑦𝑢))
2827anbi1d 623 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑢 → ((𝑦𝑡 ∧ Tr 𝑦) ↔ (𝑦𝑢 ∧ Tr 𝑦)))
29 elequ2 2169 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑢 → (𝑦𝑡𝑦𝑢))
3028, 29imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑢 → (((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3130albidv 2015 . . . . . . . . . . . . . . 15 (𝑡 = 𝑢 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3231cbvralv 3318 . . . . . . . . . . . . . 14 (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
33323anbi3i 1198 . . . . . . . . . . . . 13 ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3433abbii 2881 . . . . . . . . . . . 12 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
3534unieqi 4602 . . . . . . . . . . 11 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
3635eleq2i 2835 . . . . . . . . . 10 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
3726, 36sylnib 319 . . . . . . . . 9 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
3825, 37ax-mp 5 . . . . . . . 8 ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
39 dfon2lem7.1 . . . . . . . . . 10 𝐴 ∈ V
40 dfon2lem2 32063 . . . . . . . . . 10 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴
4139, 40ssexi 4963 . . . . . . . . 9 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ V
4241snss 4469 . . . . . . . 8 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ↔ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
4338, 42mtbi 313 . . . . . . 7 ¬ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
4443intnan 480 . . . . . 6 ¬ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
45 df-suc 5913 . . . . . . . 8 suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}})
4645sseq1i 3788 . . . . . . 7 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
47 unss 3948 . . . . . . 7 (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}) ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
4846, 47bitr4i 269 . . . . . 6 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
4944, 48mtbir 314 . . . . 5 ¬ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
5041snss 4469 . . . . . 6 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴 ↔ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴)
5145sseq1i 3788 . . . . . . . . 9 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ 𝐴)
52 unss 3948 . . . . . . . . 9 (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴) ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ 𝐴)
5351, 52bitr4i 269 . . . . . . . 8 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴))
54 dfon2lem1 32062 . . . . . . . . . . . 12 Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}
55 suctr 5990 . . . . . . . . . . . 12 (Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
5654, 55ax-mp 5 . . . . . . . . . . 11 Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}
57 vex 3352 . . . . . . . . . . . . . 14 𝑢 ∈ V
5857elsuc 5976 . . . . . . . . . . . . 13 (𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∨ 𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
59 eluni2 4597 . . . . . . . . . . . . . . 15 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ ∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥)
60 nfa1 2193 . . . . . . . . . . . . . . . 16 𝑥𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)
6131rspccv 3457 . . . . . . . . . . . . . . . . . . 19 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
62 psseq1 3854 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑥 → (𝑦𝑢𝑥𝑢))
63 treq 4916 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑥 → (Tr 𝑦 ↔ Tr 𝑥))
6462, 63anbi12d 624 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → ((𝑦𝑢 ∧ Tr 𝑦) ↔ (𝑥𝑢 ∧ Tr 𝑥)))
65 elequ1 2162 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → (𝑦𝑢𝑥𝑢))
6664, 65imbi12d 335 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → (((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
6766cbvalvw 2136 . . . . . . . . . . . . . . . . . . 19 (∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
6861, 67syl6ib 242 . . . . . . . . . . . . . . . . . 18 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
69683ad2ant3 1165 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
7015, 69sylbi 208 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
7160, 70rexlimi 3170 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
7259, 71sylbi 208 . . . . . . . . . . . . . 14 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
73 psseq1 3854 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑦𝑢𝑧𝑢))
74 treq 4916 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (Tr 𝑦 ↔ Tr 𝑧))
7573, 74anbi12d 624 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → ((𝑦𝑢 ∧ Tr 𝑦) ↔ (𝑧𝑢 ∧ Tr 𝑧)))
76 elequ1 2162 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → (𝑦𝑢𝑧𝑢))
7775, 76imbi12d 335 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑧 → (((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
7877cbvalvw 2136 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
7961, 78syl6ib 242 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
80793ad2ant3 1165 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
8115, 80sylbi 208 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
8281rexlimiv 3173 . . . . . . . . . . . . . . . . . 18 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
8359, 82sylbi 208 . . . . . . . . . . . . . . . . 17 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
8483rgen 3068 . . . . . . . . . . . . . . . 16 𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)
85 dfon2lem6 32067 . . . . . . . . . . . . . . . 16 ((Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)) → ∀𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
8654, 84, 85mp2an 683 . . . . . . . . . . . . . . 15 𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
87 psseq2 3855 . . . . . . . . . . . . . . . . . 18 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝑢𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
8887anbi1d 623 . . . . . . . . . . . . . . . . 17 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑥𝑢 ∧ Tr 𝑥) ↔ (𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥)))
89 eleq2 2832 . . . . . . . . . . . . . . . . 17 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝑢𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
9088, 89imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
9190albidv 2015 . . . . . . . . . . . . . . 15 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
9286, 91mpbiri 249 . . . . . . . . . . . . . 14 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9372, 92jaoi 883 . . . . . . . . . . . . 13 ((𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∨ 𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9458, 93sylbi 208 . . . . . . . . . . . 12 (𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9594rgen 3068 . . . . . . . . . . 11 𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)
9641sucex 7208 . . . . . . . . . . . . 13 suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ V
97 sseq1 3785 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑠𝐴 ↔ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴))
98 treq 4916 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (Tr 𝑠 ↔ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
99 raleq 3285 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
10097, 98, 993anbi123d 1560 . . . . . . . . . . . . 13 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)) ↔ (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))))
10196, 100elab 3503 . . . . . . . . . . . 12 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} ↔ (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
102 elssuni 4624 . . . . . . . . . . . 12 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))})
103101, 102sylbir 226 . . . . . . . . . . 11 ((suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)) → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))})
10456, 95, 103mp3an23 1577 . . . . . . . . . 10 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))})
105 sseq1 3785 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (𝑠𝐴𝑤𝐴))
106 treq 4916 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (Tr 𝑠 ↔ Tr 𝑤))
107 raleq 3285 . . . . . . . . . . . . . 14 (𝑠 = 𝑤 → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
108 psseq1 3854 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑥𝑢𝑦𝑢))
109 treq 4916 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (Tr 𝑥 ↔ Tr 𝑦))
110108, 109anbi12d 624 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝑥𝑢 ∧ Tr 𝑥) ↔ (𝑦𝑢 ∧ Tr 𝑦)))
111 elequ1 2162 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑥𝑢𝑦𝑢))
112110, 111imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
113112cbvalvw 2136 . . . . . . . . . . . . . . 15 (∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
114113ralbii 3126 . . . . . . . . . . . . . 14 (∀𝑢𝑤𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
115107, 114syl6bb 278 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
116105, 106, 1153anbi123d 1560 . . . . . . . . . . . 12 (𝑠 = 𝑤 → ((𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)) ↔ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))))
117116cbvabv 2889 . . . . . . . . . . 11 {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
118117unieqi 4602 . . . . . . . . . 10 {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
119104, 118syl6sseq 3810 . . . . . . . . 9 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
120119a1i 11 . . . . . . . 8 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12153, 120syl5bir 234 . . . . . . 7 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴) → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12240, 121mpani 687 . . . . . 6 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ({ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12350, 122syl5bi 233 . . . . 5 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12449, 123mtoi 190 . . . 4 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴)
125 psseq1 3854 . . . . . . . 8 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴))
126 treq 4916 . . . . . . . 8 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (Tr 𝑥 ↔ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
127125, 126anbi12d 624 . . . . . . 7 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑥𝐴 ∧ Tr 𝑥) ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
128 eleq1 2831 . . . . . . 7 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
129127, 128imbi12d 335 . . . . . 6 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) ↔ (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴)))
13041, 129spcv 3450 . . . . 5 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
13154, 130mpan2i 688 . . . 4 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
132124, 131mtod 189 . . 3 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
133 dfpss2 3852 . . . . 5 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴))
134133biimpri 219 . . . 4 (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
13540, 134mpan 681 . . 3 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
136132, 135nsyl2 144 . 2 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴)
137 eluni2 4597 . . . . 5 (𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ ∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑧𝑥)
138 psseq2 3855 . . . . . . . . . . . . . 14 (𝑡 = 𝑧 → (𝑦𝑡𝑦𝑧))
139138anbi1d 623 . . . . . . . . . . . . 13 (𝑡 = 𝑧 → ((𝑦𝑡 ∧ Tr 𝑦) ↔ (𝑦𝑧 ∧ Tr 𝑦)))
140 elequ2 2169 . . . . . . . . . . . . 13 (𝑡 = 𝑧 → (𝑦𝑡𝑦𝑧))
141139, 140imbi12d 335 . . . . . . . . . . . 12 (𝑡 = 𝑧 → (((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
142141albidv 2015 . . . . . . . . . . 11 (𝑡 = 𝑧 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
143142cbvralv 3318 . . . . . . . . . 10 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
14413, 143syl6bb 278 . . . . . . . . 9 (𝑤 = 𝑥 → (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
14511, 12, 1443anbi123d 1560 . . . . . . . 8 (𝑤 = 𝑥 → ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))))
14610, 145elab 3503 . . . . . . 7 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
147 rsp 3075 . . . . . . . 8 (∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
1481473ad2ant3 1165 . . . . . . 7 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)) → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
149146, 148sylbi 208 . . . . . 6 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
150149rexlimiv 3173 . . . . 5 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
151137, 150sylbi 208 . . . 4 (𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
152151rgen 3068 . . 3 𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)
153 raleq 3285 . . 3 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 → (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
154152, 153mpbii 224 . 2 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 → ∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
155 psseq2 3855 . . . . . 6 (𝑧 = 𝐵 → (𝑦𝑧𝑦𝐵))
156155anbi1d 623 . . . . 5 (𝑧 = 𝐵 → ((𝑦𝑧 ∧ Tr 𝑦) ↔ (𝑦𝐵 ∧ Tr 𝑦)))
157 eleq2 2832 . . . . 5 (𝑧 = 𝐵 → (𝑦𝑧𝑦𝐵))
158156, 157imbi12d 335 . . . 4 (𝑧 = 𝐵 → (((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
159158albidv 2015 . . 3 (𝑧 = 𝐵 → (∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
160159rspccv 3457 . 2 (∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) → (𝐵𝐴 → ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
161136, 154, 1603syl 18 1 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (𝐵𝐴 → ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wo 873  w3a 1107  wal 1650   = wceq 1652  wcel 2155  {cab 2750  wral 3054  wrex 3055  Vcvv 3349  cun 3729  wss 3731  wpss 3732  {csn 4333   cuni 4593  Tr wtr 4910  suc csuc 5909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pr 5061  ax-un 7146
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-v 3351  df-sbc 3596  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-pw 4316  df-sn 4334  df-pr 4336  df-uni 4594  df-iun 4677  df-tr 4911  df-suc 5913
This theorem is referenced by:  dfon2lem8  32069  dfon2  32071
  Copyright terms: Public domain W3C validator