Metamath Proof Explorer


Theorem bnj1121

Description: Technical lemma for bnj69 . 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
Hypotheses bnj1121.1 θ R FrSe A X A
bnj1121.2 τ B V TrFo B A R pred X A R B
bnj1121.3 χ n D f Fn n φ ψ
bnj1121.4 ζ i n z f i
bnj1121.5 η f K i dom f f i B
bnj1121.6 θ τ χ ζ i n η
bnj1121.7 K = f | n D f Fn n φ ψ
Assertion bnj1121 θ τ χ ζ z B

Proof

Step Hyp Ref Expression
1 bnj1121.1 θ R FrSe A X A
2 bnj1121.2 τ B V TrFo B A R pred X A R B
3 bnj1121.3 χ n D f Fn n φ ψ
4 bnj1121.4 ζ i n z f i
5 bnj1121.5 η f K i dom f f i B
6 bnj1121.6 θ τ χ ζ i n η
7 bnj1121.7 K = f | n D f Fn n φ ψ
8 19.8a χ n χ
9 8 bnj707 θ τ χ ζ n χ
10 3 7 bnj1083 f K n χ
11 9 10 sylibr θ τ χ ζ f K
12 4 simplbi ζ i n
13 12 bnj708 θ τ χ ζ i n
14 3 bnj1235 χ f Fn n
15 14 bnj707 θ τ χ ζ f Fn n
16 15 fndmd θ τ χ ζ dom f = n
17 13 16 eleqtrrd θ τ χ ζ i dom f
18 6 13 bnj1294 θ τ χ ζ η
19 18 5 sylib θ τ χ ζ f K i dom f f i B
20 11 17 19 mp2and θ τ χ ζ f i B
21 4 simprbi ζ z f i
22 21 bnj708 θ τ χ ζ z f i
23 20 22 sseldd θ τ χ ζ z B