This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfon2lem7

Description: Lemma for dfon2 . All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011)

Ref Expression
Hypothesis dfon2lem7.1 ⊢ 𝐴 ∈ V
Assertion dfon2lem7 ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( 𝐵 ∈ 𝐴 → ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 dfon2lem7.1 ⊢ 𝐴 ∈ V
2 elequ1 ⊢ ( 𝑡 = 𝑧 → ( 𝑡 ∈ 𝑡 ↔ 𝑧 ∈ 𝑡 ) )
3 elequ2 ⊢ ( 𝑡 = 𝑧 → ( 𝑧 ∈ 𝑡 ↔ 𝑧 ∈ 𝑧 ) )
4 2 3 bitrd ⊢ ( 𝑡 = 𝑧 → ( 𝑡 ∈ 𝑡 ↔ 𝑧 ∈ 𝑧 ) )
5 4 notbid ⊢ ( 𝑡 = 𝑧 → ( ¬ 𝑡 ∈ 𝑡 ↔ ¬ 𝑧 ∈ 𝑧 ) )
6 5 cbvralvw ⊢ ( ∀ 𝑡 ∈ 𝑥 ¬ 𝑡 ∈ 𝑡 ↔ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧 )
7 6 biimpi ⊢ ( ∀ 𝑡 ∈ 𝑥 ¬ 𝑡 ∈ 𝑡 → ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧 )
8 7 ralimi ⊢ ( ∀ 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∀ 𝑡 ∈ 𝑥 ¬ 𝑡 ∈ 𝑡 → ∀ 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧 )
9 untuni ⊢ ( ∀ 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ¬ 𝑧 ∈ 𝑧 ↔ ∀ 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧 )
10 8 9 sylibr ⊢ ( ∀ 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∀ 𝑡 ∈ 𝑥 ¬ 𝑡 ∈ 𝑡 → ∀ 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ¬ 𝑧 ∈ 𝑧 )
11 vex ⊢ 𝑥 ∈ V
12 sseq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐴 ) )
13 treq ⊢ ( 𝑤 = 𝑥 → ( Tr 𝑤 ↔ Tr 𝑥 ) )
14 raleq ⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ↔ ∀ 𝑡 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) )
15 12 13 14 3anbi123d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) ↔ ( 𝑥 ⊆ 𝐴 ∧ Tr 𝑥 ∧ ∀ 𝑡 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) ) )
16 11 15 elab ⊢ ( 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ↔ ( 𝑥 ⊆ 𝐴 ∧ Tr 𝑥 ∧ ∀ 𝑡 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) )
17 vex ⊢ 𝑡 ∈ V
18 dfon2lem3 ⊢ ( 𝑡 ∈ V → ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) → ( Tr 𝑡 ∧ ∀ 𝑢 ∈ 𝑡 ¬ 𝑢 ∈ 𝑢 ) ) )
19 17 18 ax-mp ⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) → ( Tr 𝑡 ∧ ∀ 𝑢 ∈ 𝑡 ¬ 𝑢 ∈ 𝑢 ) )
20 19 simprd ⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) → ∀ 𝑢 ∈ 𝑡 ¬ 𝑢 ∈ 𝑢 )
21 untelirr ⊢ ( ∀ 𝑢 ∈ 𝑡 ¬ 𝑢 ∈ 𝑢 → ¬ 𝑡 ∈ 𝑡 )
22 20 21 syl ⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) → ¬ 𝑡 ∈ 𝑡 )
23 22 ralimi ⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) → ∀ 𝑡 ∈ 𝑥 ¬ 𝑡 ∈ 𝑡 )
24 23 3ad2ant3 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ Tr 𝑥 ∧ ∀ 𝑡 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) → ∀ 𝑡 ∈ 𝑥 ¬ 𝑡 ∈ 𝑡 )
25 16 24 sylbi ⊢ ( 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ∀ 𝑡 ∈ 𝑥 ¬ 𝑡 ∈ 𝑡 )
26 10 25 mprg ⊢ ∀ 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ¬ 𝑧 ∈ 𝑧
27 untelirr ⊢ ( ∀ 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ¬ 𝑧 ∈ 𝑧 → ¬ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } )
28 psseq2 ⊢ ( 𝑡 = 𝑢 → ( 𝑦 ⊊ 𝑡 ↔ 𝑦 ⊊ 𝑢 ) )
29 28 anbi1d ⊢ ( 𝑡 = 𝑢 → ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) ↔ ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) ) )
30 elequ2 ⊢ ( 𝑡 = 𝑢 → ( 𝑦 ∈ 𝑡 ↔ 𝑦 ∈ 𝑢 ) )
31 29 30 imbi12d ⊢ ( 𝑡 = 𝑢 → ( ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ↔ ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) )
32 31 albidv ⊢ ( 𝑡 = 𝑢 → ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ↔ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) )
33 32 cbvralvw ⊢ ( ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ↔ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) )
34 33 3anbi3i ⊢ ( ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) ↔ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) )
35 34 abbii ⊢ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } = { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) }
36 35 unieqi ⊢ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) }
37 36 eleq2i ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ↔ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } )
38 27 37 sylnib ⊢ ( ∀ 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ¬ 𝑧 ∈ 𝑧 → ¬ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } )
39 26 38 ax-mp ⊢ ¬ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) }
40 dfon2lem2 ⊢ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴
41 1 40 ssexi ⊢ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ V
42 41 snss ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } ↔ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } )
43 39 42 mtbi ⊢ ¬ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) }
44 43 intnan ⊢ ¬ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } ∧ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } )
45 df-suc ⊢ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } = ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∪ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } )
46 45 sseq1i ⊢ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } ↔ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∪ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } ) ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } )
47 unss ⊢ ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } ∧ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } ) ↔ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∪ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } ) ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } )
48 46 47 bitr4i ⊢ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } ↔ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } ∧ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } ) )
49 44 48 mtbir ⊢ ¬ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) }
50 41 snss ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ 𝐴 ↔ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } ⊆ 𝐴 )
51 45 sseq1i ⊢ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴 ↔ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∪ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } ) ⊆ 𝐴 )
52 unss ⊢ ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴 ∧ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } ⊆ 𝐴 ) ↔ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∪ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } ) ⊆ 𝐴 )
53 51 52 bitr4i ⊢ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴 ↔ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴 ∧ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } ⊆ 𝐴 ) )
54 dfon2lem1 ⊢ Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) }
55 suctr ⊢ ( Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → Tr suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } )
56 54 55 ax-mp ⊢ Tr suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) }
57 vex ⊢ 𝑢 ∈ V
58 57 elsuc ⊢ ( 𝑢 ∈ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ↔ ( 𝑢 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∨ 𝑢 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ) )
59 eluni2 ⊢ ( 𝑢 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ↔ ∃ 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } 𝑢 ∈ 𝑥 )
60 nfa1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 )
61 32 rspccv ⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) → ( 𝑢 ∈ 𝑥 → ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) )
62 psseq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ⊊ 𝑢 ↔ 𝑥 ⊊ 𝑢 ) )
63 treq ⊢ ( 𝑦 = 𝑥 → ( Tr 𝑦 ↔ Tr 𝑥 ) )
64 62 63 anbi12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) ↔ ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) ) )
65 elequ1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝑢 ↔ 𝑥 ∈ 𝑢 ) )
66 64 65 imbi12d ⊢ ( 𝑦 = 𝑥 → ( ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ↔ ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) )
67 66 cbvalvw ⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ↔ ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) )
68 61 67 imbitrdi ⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) → ( 𝑢 ∈ 𝑥 → ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) )
69 68 3ad2ant3 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ Tr 𝑥 ∧ ∀ 𝑡 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) → ( 𝑢 ∈ 𝑥 → ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) )
70 16 69 sylbi ⊢ ( 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( 𝑢 ∈ 𝑥 → ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) )
71 60 70 rexlimi ⊢ ( ∃ 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } 𝑢 ∈ 𝑥 → ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) )
72 59 71 sylbi ⊢ ( 𝑢 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) )
73 psseq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ⊊ 𝑢 ↔ 𝑧 ⊊ 𝑢 ) )
74 treq ⊢ ( 𝑦 = 𝑧 → ( Tr 𝑦 ↔ Tr 𝑧 ) )
75 73 74 anbi12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) ↔ ( 𝑧 ⊊ 𝑢 ∧ Tr 𝑧 ) ) )
76 elequ1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢 ) )
77 75 76 imbi12d ⊢ ( 𝑦 = 𝑧 → ( ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ↔ ( ( 𝑧 ⊊ 𝑢 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑢 ) ) )
78 77 cbvalvw ⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ↔ ∀ 𝑧 ( ( 𝑧 ⊊ 𝑢 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑢 ) )
79 61 78 imbitrdi ⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) → ( 𝑢 ∈ 𝑥 → ∀ 𝑧 ( ( 𝑧 ⊊ 𝑢 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑢 ) ) )
80 79 3ad2ant3 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ Tr 𝑥 ∧ ∀ 𝑡 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) → ( 𝑢 ∈ 𝑥 → ∀ 𝑧 ( ( 𝑧 ⊊ 𝑢 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑢 ) ) )
81 16 80 sylbi ⊢ ( 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( 𝑢 ∈ 𝑥 → ∀ 𝑧 ( ( 𝑧 ⊊ 𝑢 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑢 ) ) )
82 81 rexlimiv ⊢ ( ∃ 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } 𝑢 ∈ 𝑥 → ∀ 𝑧 ( ( 𝑧 ⊊ 𝑢 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑢 ) )
83 59 82 sylbi ⊢ ( 𝑢 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ∀ 𝑧 ( ( 𝑧 ⊊ 𝑢 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑢 ) )
84 83 rgen ⊢ ∀ 𝑢 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∀ 𝑧 ( ( 𝑧 ⊊ 𝑢 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑢 )
85 dfon2lem6 ⊢ ( ( Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∧ ∀ 𝑢 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∀ 𝑧 ( ( 𝑧 ⊊ 𝑢 ∧ Tr 𝑧 ) → 𝑧 ∈ 𝑢 ) ) → ∀ 𝑥 ( ( 𝑥 ⊊ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∧ Tr 𝑥 ) → 𝑥 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ) )
86 54 84 85 mp2an ⊢ ∀ 𝑥 ( ( 𝑥 ⊊ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∧ Tr 𝑥 ) → 𝑥 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } )
87 psseq2 ⊢ ( 𝑢 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( 𝑥 ⊊ 𝑢 ↔ 𝑥 ⊊ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ) )
88 87 anbi1d ⊢ ( 𝑢 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) ↔ ( 𝑥 ⊊ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∧ Tr 𝑥 ) ) )
89 eleq2 ⊢ ( 𝑢 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( 𝑥 ∈ 𝑢 ↔ 𝑥 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ) )
90 88 89 imbi12d ⊢ ( 𝑢 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ↔ ( ( 𝑥 ⊊ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∧ Tr 𝑥 ) → 𝑥 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ) ) )
91 90 albidv ⊢ ( 𝑢 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ↔ ∀ 𝑥 ( ( 𝑥 ⊊ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∧ Tr 𝑥 ) → 𝑥 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ) ) )
92 86 91 mpbiri ⊢ ( 𝑢 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) )
93 72 92 jaoi ⊢ ( ( 𝑢 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∨ 𝑢 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ) → ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) )
94 58 93 sylbi ⊢ ( 𝑢 ∈ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) )
95 94 rgen ⊢ ∀ 𝑢 ∈ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 )
96 41 sucex ⊢ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ V
97 sseq1 ⊢ ( 𝑠 = suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( 𝑠 ⊆ 𝐴 ↔ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴 ) )
98 treq ⊢ ( 𝑠 = suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( Tr 𝑠 ↔ Tr suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ) )
99 raleq ⊢ ( 𝑠 = suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( ∀ 𝑢 ∈ 𝑠 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ↔ ∀ 𝑢 ∈ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) )
100 97 98 99 3anbi123d ⊢ ( 𝑠 = suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( ( 𝑠 ⊆ 𝐴 ∧ Tr 𝑠 ∧ ∀ 𝑢 ∈ 𝑠 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) ↔ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴 ∧ Tr suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∧ ∀ 𝑢 ∈ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) ) )
101 96 100 elab ⊢ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ Tr 𝑠 ∧ ∀ 𝑢 ∈ 𝑠 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) } ↔ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴 ∧ Tr suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∧ ∀ 𝑢 ∈ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) )
102 elssuni ⊢ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ Tr 𝑠 ∧ ∀ 𝑢 ∈ 𝑠 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) } → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ ∪ { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ Tr 𝑠 ∧ ∀ 𝑢 ∈ 𝑠 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) } )
103 101 102 sylbir ⊢ ( ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴 ∧ Tr suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∧ ∀ 𝑢 ∈ suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ ∪ { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ Tr 𝑠 ∧ ∀ 𝑢 ∈ 𝑠 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) } )
104 56 95 103 mp3an23 ⊢ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴 → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ ∪ { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ Tr 𝑠 ∧ ∀ 𝑢 ∈ 𝑠 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) } )
105 sseq1 ⊢ ( 𝑠 = 𝑤 → ( 𝑠 ⊆ 𝐴 ↔ 𝑤 ⊆ 𝐴 ) )
106 treq ⊢ ( 𝑠 = 𝑤 → ( Tr 𝑠 ↔ Tr 𝑤 ) )
107 raleq ⊢ ( 𝑠 = 𝑤 → ( ∀ 𝑢 ∈ 𝑠 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ↔ ∀ 𝑢 ∈ 𝑤 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) )
108 psseq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊊ 𝑢 ↔ 𝑦 ⊊ 𝑢 ) )
109 treq ⊢ ( 𝑥 = 𝑦 → ( Tr 𝑥 ↔ Tr 𝑦 ) )
110 108 109 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) ↔ ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) ) )
111 elequ1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑢 ↔ 𝑦 ∈ 𝑢 ) )
112 110 111 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ↔ ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) )
113 112 cbvalvw ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ↔ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) )
114 113 ralbii ⊢ ( ∀ 𝑢 ∈ 𝑤 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ↔ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) )
115 107 114 bitrdi ⊢ ( 𝑠 = 𝑤 → ( ∀ 𝑢 ∈ 𝑠 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ↔ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) )
116 105 106 115 3anbi123d ⊢ ( 𝑠 = 𝑤 → ( ( 𝑠 ⊆ 𝐴 ∧ Tr 𝑠 ∧ ∀ 𝑢 ∈ 𝑠 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) ↔ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) ) )
117 116 cbvabv ⊢ { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ Tr 𝑠 ∧ ∀ 𝑢 ∈ 𝑠 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) } = { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) }
118 117 unieqi ⊢ ∪ { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ Tr 𝑠 ∧ ∀ 𝑢 ∈ 𝑠 ∀ 𝑥 ( ( 𝑥 ⊊ 𝑢 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝑢 ) ) } = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) }
119 104 118 sseqtrdi ⊢ ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴 → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } )
120 119 a1i ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴 → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } ) )
121 53 120 biimtrrid ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴 ∧ { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } ⊆ 𝐴 ) → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } ) )
122 40 121 mpani ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( { ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } } ⊆ 𝐴 → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } ) )
123 50 122 biimtrid ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ 𝐴 → suc ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑢 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑢 ) ) } ) )
124 49 123 mtoi ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ¬ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ 𝐴 )
125 psseq1 ⊢ ( 𝑥 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( 𝑥 ⊊ 𝐴 ↔ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊊ 𝐴 ) )
126 treq ⊢ ( 𝑥 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( Tr 𝑥 ↔ Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ) )
127 125 126 anbi12d ⊢ ( 𝑥 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) ↔ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊊ 𝐴 ∧ Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ) ) )
128 eleq1 ⊢ ( 𝑥 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( 𝑥 ∈ 𝐴 ↔ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ 𝐴 ) )
129 127 128 imbi12d ⊢ ( 𝑥 = ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ↔ ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊊ 𝐴 ∧ Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ) → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ 𝐴 ) ) )
130 41 129 spcv ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊊ 𝐴 ∧ Tr ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ) → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ 𝐴 ) )
131 54 130 mpan2i ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊊ 𝐴 → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∈ 𝐴 ) )
132 124 131 mtod ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ¬ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊊ 𝐴 )
133 dfpss2 ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊊ 𝐴 ↔ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴 ∧ ¬ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } = 𝐴 ) )
134 133 biimpri ⊢ ( ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊆ 𝐴 ∧ ¬ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } = 𝐴 ) → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊊ 𝐴 )
135 40 134 mpan ⊢ ( ¬ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } = 𝐴 → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ⊊ 𝐴 )
136 132 135 nsyl2 ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } = 𝐴 )
137 eluni2 ⊢ ( 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ↔ ∃ 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } 𝑧 ∈ 𝑥 )
138 psseq2 ⊢ ( 𝑡 = 𝑧 → ( 𝑦 ⊊ 𝑡 ↔ 𝑦 ⊊ 𝑧 ) )
139 138 anbi1d ⊢ ( 𝑡 = 𝑧 → ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) ↔ ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) ) )
140 elequ2 ⊢ ( 𝑡 = 𝑧 → ( 𝑦 ∈ 𝑡 ↔ 𝑦 ∈ 𝑧 ) )
141 139 140 imbi12d ⊢ ( 𝑡 = 𝑧 → ( ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ↔ ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) ) )
142 141 albidv ⊢ ( 𝑡 = 𝑧 → ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ↔ ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) ) )
143 142 cbvralvw ⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ↔ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) )
144 14 143 bitrdi ⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ↔ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) ) )
145 12 13 144 3anbi123d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) ↔ ( 𝑥 ⊆ 𝐴 ∧ Tr 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) ) ) )
146 11 145 elab ⊢ ( 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ↔ ( 𝑥 ⊆ 𝐴 ∧ Tr 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) ) )
147 rsp ⊢ ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) → ( 𝑧 ∈ 𝑥 → ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) ) )
148 147 3ad2ant3 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ Tr 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) ) → ( 𝑧 ∈ 𝑥 → ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) ) )
149 146 148 sylbi ⊢ ( 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ( 𝑧 ∈ 𝑥 → ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) ) )
150 149 rexlimiv ⊢ ( ∃ 𝑥 ∈ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } 𝑧 ∈ 𝑥 → ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) )
151 137 150 sylbi ⊢ ( 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } → ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) )
152 151 rgen ⊢ ∀ 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 )
153 raleq ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } = 𝐴 → ( ∀ 𝑧 ∈ ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) ) )
154 152 153 mpbii ⊢ ( ∪ { 𝑤 ∣ ( 𝑤 ⊆ 𝐴 ∧ Tr 𝑤 ∧ ∀ 𝑡 ∈ 𝑤 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑡 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑡 ) ) } = 𝐴 → ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) )
155 psseq2 ⊢ ( 𝑧 = 𝐵 → ( 𝑦 ⊊ 𝑧 ↔ 𝑦 ⊊ 𝐵 ) )
156 155 anbi1d ⊢ ( 𝑧 = 𝐵 → ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) ↔ ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) ) )
157 eleq2 ⊢ ( 𝑧 = 𝐵 → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝐵 ) )
158 156 157 imbi12d ⊢ ( 𝑧 = 𝐵 → ( ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) ↔ ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) )
159 158 albidv ⊢ ( 𝑧 = 𝐵 → ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) ↔ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) )
160 159 rspccv ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑧 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑧 ) → ( 𝐵 ∈ 𝐴 → ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) )
161 136 154 160 3syl ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( 𝐵 ∈ 𝐴 → ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) )