Metamath Proof Explorer

Theorem bnj1318

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj1318 ⊢ 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 hbab1 ⊢ z ∈ 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 z ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
7 hbab1 ⊢ z ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred Y A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R → ∀ f z ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred Y A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
8 6 7 bnj1316 ⊢ 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 → ⋃ 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
9 5 8 syl ⊢ 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
10 biid ⊢ f ⁡ ∅ = pred X A R ↔ f ⁡ ∅ = pred X A R
11 biid ⊢ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
12 eqid ⊢ ω ∖ ∅ = ω ∖ ∅
13 eqid ⊢ 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 X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
14 10 11 12 13 bnj882 ⊢ 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
15 biid ⊢ f ⁡ ∅ = pred Y A R ↔ f ⁡ ∅ = pred Y A R
16 eqid ⊢ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred Y 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
17 15 11 12 16 bnj882 ⊢ 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
18 9 14 17 3eqtr4g ⊢ X = Y → trCl X A R = trCl Y A R