Metamath Proof Explorer

Theorem bnj1147

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj1147 ⊢ trCl X A R ⊆ A

Proof

Step Hyp Ref Expression
1 biid ⊢ f ⁡ ∅ = pred X A R ↔ f ⁡ ∅ = pred X A R
2 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
3 eqid ⊢ ω ∖ ∅ = ω ∖ ∅
4 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
5 biid ⊢ 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 X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
6 biid ⊢ i ≠ ∅ ∧ i ∈ n ∧ n ∈ ω ∖ ∅ ∧ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ∧ j ∈ n ∧ i = suc ⁡ j ↔ i ≠ ∅ ∧ i ∈ n ∧ n ∈ ω ∖ ∅ ∧ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ∧ j ∈ n ∧ i = suc ⁡ j
7 1 2 3 4 5 6 bnj1145 ⊢ trCl X A R ⊆ A