Metamath Proof Explorer

Theorem bnj1029

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

Ref Expression
Assertion bnj1029 ⊢ R FrSe A ∧ X ∈ A → TrFo trCl X A R A R

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 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
4 biid ⊢ R FrSe A ∧ X ∈ A ∧ y ∈ trCl X A R ∧ z ∈ pred y A R ↔ R FrSe A ∧ X ∈ A ∧ y ∈ trCl X A R ∧ z ∈ pred y A R
5 biid ⊢ m ∈ ω ∧ n = suc ⁡ m ∧ p = suc ⁡ n ↔ m ∈ ω ∧ n = suc ⁡ m ∧ p = suc ⁡ n
6 biid ⊢ i ∈ n ∧ y ∈ f ⁡ i ↔ i ∈ n ∧ y ∈ f ⁡ i
7 biid ⊢ [˙p / n]˙ f ⁡ ∅ = pred X A R ↔ [˙p / n]˙ f ⁡ ∅ = pred X A R
8 biid ⊢ [˙p / n]˙ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ↔ [˙p / n]˙ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
9 biid ⊢ [˙p / n]˙ n ∈ ω ∖ ∅ ∧ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ↔ [˙p / n]˙ n ∈ ω ∖ ∅ ∧ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
10 biid ⊢ [˙ f ∪ n ⋃ y ∈ f ⁡ m pred y A R / f]˙ [˙p / n]˙ f ⁡ ∅ = pred X A R ↔ [˙ f ∪ n ⋃ y ∈ f ⁡ m pred y A R / f]˙ [˙p / n]˙ f ⁡ ∅ = pred X A R
11 biid ⊢ [˙ f ∪ n ⋃ y ∈ f ⁡ m pred y A R / f]˙ [˙p / n]˙ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ↔ [˙ f ∪ n ⋃ y ∈ f ⁡ m pred y A R / f]˙ [˙p / n]˙ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
12 biid ⊢ [˙ f ∪ n ⋃ y ∈ f ⁡ m pred y A R / f]˙ [˙p / n]˙ 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 ⋃ y ∈ f ⁡ m pred y A R / f]˙ [˙p / n]˙ n ∈ ω ∖ ∅ ∧ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
13 eqid ⊢ ω ∖ ∅ = ω ∖ ∅
14 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
15 eqid ⊢ ⋃ y ∈ f ⁡ m pred y A R = ⋃ y ∈ f ⁡ m pred y A R
16 eqid ⊢ f ∪ n ⋃ y ∈ f ⁡ m pred y A R = f ∪ n ⋃ y ∈ f ⁡ m pred y A R
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 bnj907 ⊢ R FrSe A ∧ X ∈ A → TrFo trCl X A R A R