Metamath Proof Explorer


Theorem bnj18eq1

Description: Equality theorem for transitive closure. (Contributed by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Assertion bnj18eq1 ( 𝑋 = 𝑌 → trCl ( 𝑋 , 𝐴 , 𝑅 ) = trCl ( 𝑌 , 𝐴 , 𝑅 ) )

Proof

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 ( 𝑌 , 𝐴 , 𝑅 ) )