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 ⊢ X = Y → trCl X A R = trCl Y A R

Proof

Step Hyp Ref Expression
1 bnj602 ⊢ X = Y → pred X A R = pred Y A R
2 1 eqeq2d ⊢ X = Y → f ⁡ ∅ = pred X A R ↔ f ⁡ ∅ = pred Y A R
3 2 3anbi2d ⊢ X = Y → f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ↔ f Fn n ∧ f ⁡ ∅ = pred Y A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
4 3 rexbidv ⊢ X = Y → ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ↔ ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred Y A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
5 4 abbidv ⊢ X = Y → f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R = f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred Y A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
6 5 eleq2d ⊢ X = Y → f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ↔ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred Y A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
7 6 anbi1d ⊢ X = Y → f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ∧ x ∈ ⋃ i ∈ dom ⁡ f f ⁡ i ↔ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred Y A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ∧ x ∈ ⋃ i ∈ dom ⁡ f f ⁡ i
8 7 rexbidv2 ⊢ X = Y → ∃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R x ∈ ⋃ i ∈ dom ⁡ f f ⁡ i ↔ ∃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred Y A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R x ∈ ⋃ i ∈ dom ⁡ f f ⁡ i
9 8 abbidv ⊢ X = Y → x | ∃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R x ∈ ⋃ i ∈ dom ⁡ f f ⁡ i = x | ∃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred Y A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R x ∈ ⋃ i ∈ dom ⁡ f f ⁡ i
10 df-iun ⊢ ⋃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ⋃ i ∈ dom ⁡ f f ⁡ i = x | ∃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R x ∈ ⋃ i ∈ dom ⁡ f f ⁡ i
11 df-iun ⊢ ⋃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred Y A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ⋃ i ∈ dom ⁡ f f ⁡ i = x | ∃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred Y A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R x ∈ ⋃ i ∈ dom ⁡ f f ⁡ i
12 9 10 11 3eqtr4g ⊢ X = Y → ⋃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ⋃ i ∈ dom ⁡ f f ⁡ i = ⋃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred Y A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ⋃ i ∈ dom ⁡ f f ⁡ i
13 df-bnj18 ⊢ trCl X A R = ⋃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ⋃ i ∈ dom ⁡ f f ⁡ i
14 df-bnj18 ⊢ trCl Y A R = ⋃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred Y A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ⋃ i ∈ dom ⁡ f f ⁡ i
15 12 13 14 3eqtr4g ⊢ X = Y → trCl X A R = trCl Y A R