Step |
Hyp |
Ref |
Expression |
1 |
|
bnj602 |
⊢ ( 𝑋 = 𝑌 → pred ( 𝑋 , 𝐴 , 𝑅 ) = pred ( 𝑌 , 𝐴 , 𝑅 ) ) |
2 |
1
|
eqeq2d |
⊢ ( 𝑋 = 𝑌 → ( ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑌 , 𝐴 , 𝑅 ) ) ) |
3 |
2
|
3anbi2d |
⊢ ( 𝑋 = 𝑌 → ( ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑌 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) ) |
4 |
3
|
rexbidv |
⊢ ( 𝑋 = 𝑌 → ( ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑌 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) ) |
5 |
4
|
abbidv |
⊢ ( 𝑋 = 𝑌 → { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } = { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑌 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ) |
6 |
5
|
eleq2d |
⊢ ( 𝑋 = 𝑌 → ( 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ↔ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑌 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ) ) |
7 |
6
|
anbi1d |
⊢ ( 𝑋 = 𝑌 → ( ( 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∧ 𝑥 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑌 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∧ 𝑥 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ) ) ) |
8 |
7
|
rexbidv2 |
⊢ ( 𝑋 = 𝑌 → ( ∃ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑥 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ↔ ∃ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑌 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑥 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ) ) |
9 |
8
|
abbidv |
⊢ ( 𝑋 = 𝑌 → { 𝑥 ∣ ∃ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑥 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) } = { 𝑥 ∣ ∃ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑌 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑥 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) } ) |
10 |
|
df-iun |
⊢ ∪ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) = { 𝑥 ∣ ∃ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑥 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) } |
11 |
|
df-iun |
⊢ ∪ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑌 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) = { 𝑥 ∣ ∃ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑌 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } 𝑥 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) } |
12 |
9 10 11
|
3eqtr4g |
⊢ ( 𝑋 = 𝑌 → ∪ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) = ∪ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑌 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ) |
13 |
|
df-bnj18 |
⊢ trCl ( 𝑋 , 𝐴 , 𝑅 ) = ∪ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) |
14 |
|
df-bnj18 |
⊢ trCl ( 𝑌 , 𝐴 , 𝑅 ) = ∪ 𝑓 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ( ω ∖ { ∅ } ) ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑌 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) } ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) |
15 |
12 13 14
|
3eqtr4g |
⊢ ( 𝑋 = 𝑌 → trCl ( 𝑋 , 𝐴 , 𝑅 ) = trCl ( 𝑌 , 𝐴 , 𝑅 ) ) |