Metamath Proof Explorer

Theorem bnj1124

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

Ref Expression
Hypotheses bnj1124.4 ⊢ θ ↔ R FrSe A ∧ X ∈ A
bnj1124.5 ⊢ τ ↔ B ∈ V ∧ TrFo B A R ∧ pred X A R ⊆ B
Assertion bnj1124 ⊢ θ ∧ τ → trCl X A R ⊆ B

Proof

Step Hyp Ref Expression
1 bnj1124.4 ⊢ θ ↔ R FrSe A ∧ X ∈ A
2 bnj1124.5 ⊢ τ ↔ B ∈ V ∧ TrFo B A R ∧ pred X A R ⊆ B
3 biid ⊢ f ⁡ ∅ = pred X A R ↔ f ⁡ ∅ = pred X A R
4 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
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 ∈ n ∧ z ∈ f ⁡ i ↔ i ∈ n ∧ z ∈ f ⁡ i
7 eqid ⊢ ω ∖ ∅ = ω ∖ ∅
8 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
9 biid ⊢ 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 ⊆ B ↔ 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 ⊆ B
10 biid ⊢ ∀ j ∈ n j E i → [˙j / i]˙ 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 ⊆ B ↔ ∀ j ∈ n j E i → [˙j / i]˙ 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 ⊆ B
11 biid ⊢ [˙j / i]˙ f ⁡ ∅ = pred X A R ↔ [˙j / i]˙ f ⁡ ∅ = pred X A R
12 biid ⊢ [˙j / i]˙ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ↔ [˙j / i]˙ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
13 biid ⊢ [˙j / i]˙ n ∈ ω ∖ ∅ ∧ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ↔ [˙j / i]˙ n ∈ ω ∖ ∅ ∧ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
14 biid ⊢ [˙j / i]˙ θ ↔ [˙j / i]˙ θ
15 biid ⊢ [˙j / i]˙ τ ↔ [˙j / i]˙ τ
16 biid ⊢ [˙j / i]˙ i ∈ n ∧ z ∈ f ⁡ i ↔ [˙j / i]˙ i ∈ n ∧ z ∈ f ⁡ i
17 biid ⊢ [˙j / i]˙ 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 ⊆ B ↔ [˙j / i]˙ 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 ⊆ B
18 biid ⊢ j ∈ n ∧ j E i → [˙j / i]˙ 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 ⊆ B ↔ j ∈ n ∧ j E i → [˙j / i]˙ 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 ⊆ B
19 biid ⊢ i ∈ n ∧ j ∈ n ∧ j E i → [˙j / i]˙ 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 ⊆ B ∧ 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 ↔ i ∈ n ∧ j ∈ n ∧ j E i → [˙j / i]˙ 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 ⊆ B ∧ 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
20 3 4 5 1 2 6 7 8 9 10 11 12 13 14 15 16 17 18 19 bnj1030 ⊢ θ ∧ τ → trCl X A R ⊆ B