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