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 30744
Description: Lemma for dfon2 30747. 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 1983 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑧 → (𝑡𝑡𝑧𝑡))
2 elequ2 1990 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑧 → (𝑧𝑡𝑧𝑧))
31, 2bitrd 266 . . . . . . . . . . . . . . 15 (𝑡 = 𝑧 → (𝑡𝑡𝑧𝑧))
43notbid 306 . . . . . . . . . . . . . 14 (𝑡 = 𝑧 → (¬ 𝑡𝑡 ↔ ¬ 𝑧𝑧))
54cbvralv 3146 . . . . . . . . . . . . 13 (∀𝑡𝑥 ¬ 𝑡𝑡 ↔ ∀𝑧𝑥 ¬ 𝑧𝑧)
65biimpi 204 . . . . . . . . . . . 12 (∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑧𝑥 ¬ 𝑧𝑧)
76ralimi 2935 . . . . . . . . . . 11 (∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧𝑥 ¬ 𝑧𝑧)
8 untuni 30646 . . . . . . . . . . 11 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 ↔ ∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧𝑥 ¬ 𝑧𝑧)
97, 8sylibr 222 . . . . . . . . . 10 (∀𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑡𝑥 ¬ 𝑡𝑡 → ∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧)
10 vex 3175 . . . . . . . . . . . 12 𝑥 ∈ V
11 sseq1 3588 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑤𝐴𝑥𝐴))
12 treq 4680 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (Tr 𝑤 ↔ Tr 𝑥))
13 raleq 3114 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
1411, 12, 133anbi123d 1390 . . . . . . . . . . . 12 (𝑤 = 𝑥 → ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))))
1510, 14elab 3318 . . . . . . . . . . 11 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)))
16 vex 3175 . . . . . . . . . . . . . . . 16 𝑡 ∈ V
17 dfon2lem3 30740 . . . . . . . . . . . . . . . 16 (𝑡 ∈ V → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝑡 ∧ ∀𝑢𝑡 ¬ 𝑢𝑢)))
1816, 17ax-mp 5 . . . . . . . . . . . . . . 15 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (Tr 𝑡 ∧ ∀𝑢𝑡 ¬ 𝑢𝑢))
1918simprd 477 . . . . . . . . . . . . . 14 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ∀𝑢𝑡 ¬ 𝑢𝑢)
20 untelirr 30645 . . . . . . . . . . . . . 14 (∀𝑢𝑡 ¬ 𝑢𝑢 → ¬ 𝑡𝑡)
2119, 20syl 17 . . . . . . . . . . . . 13 (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ¬ 𝑡𝑡)
2221ralimi 2935 . . . . . . . . . . . 12 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → ∀𝑡𝑥 ¬ 𝑡𝑡)
23223ad2ant3 1076 . . . . . . . . . . 11 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → ∀𝑡𝑥 ¬ 𝑡𝑡)
2415, 23sylbi 205 . . . . . . . . . 10 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑡𝑥 ¬ 𝑡𝑡)
259, 24mprg 2909 . . . . . . . . 9 𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧
26 untelirr 30645 . . . . . . . . . 10 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
27 psseq2 3656 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑢 → (𝑦𝑡𝑦𝑢))
2827anbi1d 736 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑢 → ((𝑦𝑡 ∧ Tr 𝑦) ↔ (𝑦𝑢 ∧ Tr 𝑦)))
29 elequ2 1990 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑢 → (𝑦𝑡𝑦𝑢))
3028, 29imbi12d 332 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑢 → (((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3130albidv 1835 . . . . . . . . . . . . . . 15 (𝑡 = 𝑢 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3231cbvralv 3146 . . . . . . . . . . . . . 14 (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
33323anbi3i 1247 . . . . . . . . . . . . 13 ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
3433abbii 2725 . . . . . . . . . . . 12 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
3534unieqi 4375 . . . . . . . . . . 11 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
3635eleq2i 2679 . . . . . . . . . 10 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
3726, 36sylnib 316 . . . . . . . . 9 (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ¬ 𝑧𝑧 → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
3825, 37ax-mp 5 . . . . . . . 8 ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
39 dfon2lem7.1 . . . . . . . . . 10 𝐴 ∈ V
40 dfon2lem2 30739 . . . . . . . . . 10 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴
4139, 40ssexi 4726 . . . . . . . . 9 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ V
4241snss 4258 . . . . . . . 8 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ↔ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
4338, 42mtbi 310 . . . . . . 7 ¬ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
4443intnan 950 . . . . . 6 ¬ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
45 df-suc 5632 . . . . . . . 8 suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}})
4645sseq1i 3591 . . . . . . 7 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
47 unss 3748 . . . . . . 7 (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}) ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
4846, 47bitr4i 265 . . . . . 6 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))} ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
4944, 48mtbir 311 . . . . 5 ¬ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
5041snss 4258 . . . . . 6 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴 ↔ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴)
5145sseq1i 3591 . . . . . . . . 9 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ 𝐴)
52 unss 3748 . . . . . . . . 9 (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴) ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∪ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}}) ⊆ 𝐴)
5351, 52bitr4i 265 . . . . . . . 8 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴))
54 dfon2lem1 30738 . . . . . . . . . . . 12 Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}
55 suctr 5711 . . . . . . . . . . . 12 (Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
5654, 55ax-mp 5 . . . . . . . . . . 11 Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}
57 vex 3175 . . . . . . . . . . . . . 14 𝑢 ∈ V
5857elsuc 5697 . . . . . . . . . . . . 13 (𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∨ 𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
59 eluni2 4370 . . . . . . . . . . . . . . 15 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ ∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥)
60 nfa1 2014 . . . . . . . . . . . . . . . 16 𝑥𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)
6131rspccv 3278 . . . . . . . . . . . . . . . . . . 19 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
62 psseq1 3655 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑥 → (𝑦𝑢𝑥𝑢))
63 treq 4680 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑥 → (Tr 𝑦 ↔ Tr 𝑥))
6462, 63anbi12d 742 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → ((𝑦𝑢 ∧ Tr 𝑦) ↔ (𝑥𝑢 ∧ Tr 𝑥)))
65 elequ1 1983 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → (𝑦𝑢𝑥𝑢))
6664, 65imbi12d 332 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → (((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
6766cbvalv 2260 . . . . . . . . . . . . . . . . . . 19 (∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
6861, 67syl6ib 239 . . . . . . . . . . . . . . . . . 18 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
69683ad2ant3 1076 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
7015, 69sylbi 205 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
7160, 70rexlimi 3005 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥 → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
7259, 71sylbi 205 . . . . . . . . . . . . . 14 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
73 psseq1 3655 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑦𝑢𝑧𝑢))
74 treq 4680 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (Tr 𝑦 ↔ Tr 𝑧))
7573, 74anbi12d 742 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → ((𝑦𝑢 ∧ Tr 𝑦) ↔ (𝑧𝑢 ∧ Tr 𝑧)))
76 elequ1 1983 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → (𝑦𝑢𝑧𝑢))
7775, 76imbi12d 332 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑧 → (((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
7877cbvalv 2260 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢) ↔ ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
7961, 78syl6ib 239 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
80793ad2ant3 1076 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
8115, 80sylbi 205 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)))
8281rexlimiv 3008 . . . . . . . . . . . . . . . . . 18 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑢𝑥 → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
8359, 82sylbi 205 . . . . . . . . . . . . . . . . 17 (𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢))
8483rgen 2905 . . . . . . . . . . . . . . . 16 𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)
85 dfon2lem6 30743 . . . . . . . . . . . . . . . 16 ((Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑧((𝑧𝑢 ∧ Tr 𝑧) → 𝑧𝑢)) → ∀𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
8654, 84, 85mp2an 703 . . . . . . . . . . . . . . 15 𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})
87 psseq2 3656 . . . . . . . . . . . . . . . . . 18 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝑢𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
8887anbi1d 736 . . . . . . . . . . . . . . . . 17 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑥𝑢 ∧ Tr 𝑥) ↔ (𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥)))
89 eleq2 2676 . . . . . . . . . . . . . . . . 17 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝑢𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
9088, 89imbi12d 332 . . . . . . . . . . . . . . . 16 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
9190albidv 1835 . . . . . . . . . . . . . . 15 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑥((𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ Tr 𝑥) → 𝑥 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
9286, 91mpbiri 246 . . . . . . . . . . . . . 14 (𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9372, 92jaoi 392 . . . . . . . . . . . . 13 ((𝑢 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∨ 𝑢 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9458, 93sylbi 205 . . . . . . . . . . . 12 (𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))
9594rgen 2905 . . . . . . . . . . 11 𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)
9641sucex 6880 . . . . . . . . . . . . 13 suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ V
97 sseq1 3588 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑠𝐴 ↔ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴))
98 treq 4680 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (Tr 𝑠 ↔ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
99 raleq 3114 . . . . . . . . . . . . . 14 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
10097, 98, 993anbi123d 1390 . . . . . . . . . . . . 13 (𝑠 = suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)) ↔ (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))))
10196, 100elab 3318 . . . . . . . . . . . 12 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} ↔ (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
102 elssuni 4397 . . . . . . . . . . . 12 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))})
103101, 102sylbir 223 . . . . . . . . . . 11 ((suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ Tr suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∧ ∀𝑢 ∈ suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)) → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))})
10456, 95, 103mp3an23 1407 . . . . . . . . . 10 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))})
105 sseq1 3588 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (𝑠𝐴𝑤𝐴))
106 treq 4680 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (Tr 𝑠 ↔ Tr 𝑤))
107 raleq 3114 . . . . . . . . . . . . . 14 (𝑠 = 𝑤 → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)))
108 psseq1 3655 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑥𝑢𝑦𝑢))
109 treq 4680 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (Tr 𝑥 ↔ Tr 𝑦))
110108, 109anbi12d 742 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝑥𝑢 ∧ Tr 𝑥) ↔ (𝑦𝑢 ∧ Tr 𝑦)))
111 elequ1 1983 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑥𝑢𝑦𝑢))
112110, 111imbi12d 332 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
113112cbvalv 2260 . . . . . . . . . . . . . . 15 (∀𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
114113ralbii 2962 . . . . . . . . . . . . . 14 (∀𝑢𝑤𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))
115107, 114syl6bb 274 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢) ↔ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢)))
116105, 106, 1153anbi123d 1390 . . . . . . . . . . . 12 (𝑠 = 𝑤 → ((𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢)) ↔ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))))
117116cbvabv 2733 . . . . . . . . . . 11 {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
118117unieqi 4375 . . . . . . . . . 10 {𝑠 ∣ (𝑠𝐴 ∧ Tr 𝑠 ∧ ∀𝑢𝑠𝑥((𝑥𝑢 ∧ Tr 𝑥) → 𝑥𝑢))} = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}
119104, 118syl6sseq 3613 . . . . . . . . 9 (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))})
120119a1i 11 . . . . . . . 8 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12153, 120syl5bir 231 . . . . . . 7 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ { {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴) → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12240, 121mpani 707 . . . . . 6 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ({ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}} ⊆ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12350, 122syl5bi 230 . . . . 5 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴 → suc {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑢𝑤𝑦((𝑦𝑢 ∧ Tr 𝑦) → 𝑦𝑢))}))
12449, 123mtoi 188 . . . 4 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴)
125 psseq1 3655 . . . . . . . 8 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴))
126 treq 4680 . . . . . . . 8 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (Tr 𝑥 ↔ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}))
127125, 126anbi12d 742 . . . . . . 7 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ((𝑥𝐴 ∧ Tr 𝑥) ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))})))
128 eleq1 2675 . . . . . . 7 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑥𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
129127, 128imbi12d 332 . . . . . 6 (𝑥 = {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) ↔ (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴)))
13041, 129spcv 3271 . . . . 5 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ∧ Tr {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
13154, 130mpan2i 708 . . . 4 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ∈ 𝐴))
132124, 131mtod 187 . . 3 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
133 dfpss2 3653 . . . . 5 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴 ↔ ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴))
134133biimpri 216 . . . 4 (( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊆ 𝐴 ∧ ¬ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
13540, 134mpan 701 . . 3 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ⊊ 𝐴)
136132, 135nsyl2 140 . 2 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴)
137 eluni2 4370 . . . . 5 (𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ ∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑧𝑥)
138 psseq2 3656 . . . . . . . . . . . . . 14 (𝑡 = 𝑧 → (𝑦𝑡𝑦𝑧))
139138anbi1d 736 . . . . . . . . . . . . 13 (𝑡 = 𝑧 → ((𝑦𝑡 ∧ Tr 𝑦) ↔ (𝑦𝑧 ∧ Tr 𝑦)))
140 elequ2 1990 . . . . . . . . . . . . 13 (𝑡 = 𝑧 → (𝑦𝑡𝑦𝑧))
141139, 140imbi12d 332 . . . . . . . . . . . 12 (𝑡 = 𝑧 → (((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
142141albidv 1835 . . . . . . . . . . 11 (𝑡 = 𝑧 → (∀𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
143142cbvralv 3146 . . . . . . . . . 10 (∀𝑡𝑥𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
14413, 143syl6bb 274 . . . . . . . . 9 (𝑤 = 𝑥 → (∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡) ↔ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
14511, 12, 1443anbi123d 1390 . . . . . . . 8 (𝑤 = 𝑥 → ((𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡)) ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))))
14610, 145elab 3318 . . . . . . 7 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} ↔ (𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
147 rsp 2912 . . . . . . . 8 (∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
1481473ad2ant3 1076 . . . . . . 7 ((𝑥𝐴 ∧ Tr 𝑥 ∧ ∀𝑧𝑥𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)) → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
149146, 148sylbi 205 . . . . . 6 (𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → (𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
150149rexlimiv 3008 . . . . 5 (∃𝑥 ∈ {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}𝑧𝑥 → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
151137, 150sylbi 205 . . . 4 (𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} → ∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
152151rgen 2905 . . 3 𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)
153 raleq 3114 . . 3 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 → (∀𝑧 {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))}∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧)))
154152, 153mpbii 221 . 2 ( {𝑤 ∣ (𝑤𝐴 ∧ Tr 𝑤 ∧ ∀𝑡𝑤𝑦((𝑦𝑡 ∧ Tr 𝑦) → 𝑦𝑡))} = 𝐴 → ∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧))
155 psseq2 3656 . . . . . 6 (𝑧 = 𝐵 → (𝑦𝑧𝑦𝐵))
156155anbi1d 736 . . . . 5 (𝑧 = 𝐵 → ((𝑦𝑧 ∧ Tr 𝑦) ↔ (𝑦𝐵 ∧ Tr 𝑦)))
157 eleq2 2676 . . . . 5 (𝑧 = 𝐵 → (𝑦𝑧𝑦𝐵))
158156, 157imbi12d 332 . . . 4 (𝑧 = 𝐵 → (((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
159158albidv 1835 . . 3 (𝑧 = 𝐵 → (∀𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) ↔ ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
160159rspccv 3278 . 2 (∀𝑧𝐴𝑦((𝑦𝑧 ∧ Tr 𝑦) → 𝑦𝑧) → (𝐵𝐴 → ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
161136, 154, 1603syl 18 1 (∀𝑥((𝑥𝐴 ∧ Tr 𝑥) → 𝑥𝐴) → (𝐵𝐴 → ∀𝑦((𝑦𝐵 ∧ Tr 𝑦) → 𝑦𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 381  wa 382  w3a 1030  wal 1472   = wceq 1474  wcel 1976  {cab 2595  wral 2895  wrex 2896  Vcvv 3172  cun 3537  wss 3539  wpss 3540  {csn 4124   cuni 4366  Tr wtr 4674  suc csuc 5628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-pw 4109  df-sn 4125  df-pr 4127  df-uni 4367  df-iun 4451  df-tr 4675  df-suc 5632
This theorem is referenced by:  dfon2lem8  30745  dfon2  30747
  Copyright terms: Public domain W3C validator