Metamath Proof Explorer


Theorem bnj545

Description: Technical lemma for bnj852 . 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 bnj545.1 ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
bnj545.2 𝐷 = ( ω ∖ { ∅ } )
bnj545.3 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝑦 ∈ ( 𝑓𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
bnj545.4 ( 𝜏 ↔ ( 𝑓 Fn 𝑚𝜑′𝜓′ ) )
bnj545.5 ( 𝜎 ↔ ( 𝑚𝐷𝑛 = suc 𝑚𝑝𝑚 ) )
bnj545.6 ( ( 𝑅 FrSe 𝐴𝜏𝜎 ) → 𝐺 Fn 𝑛 )
bnj545.7 ( 𝜑″ ↔ ( 𝐺 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
Assertion bnj545 ( ( 𝑅 FrSe 𝐴𝜏𝜎 ) → 𝜑″ )

Proof

Step Hyp Ref Expression
1 bnj545.1 ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2 bnj545.2 𝐷 = ( ω ∖ { ∅ } )
3 bnj545.3 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝑦 ∈ ( 𝑓𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
4 bnj545.4 ( 𝜏 ↔ ( 𝑓 Fn 𝑚𝜑′𝜓′ ) )
5 bnj545.5 ( 𝜎 ↔ ( 𝑚𝐷𝑛 = suc 𝑚𝑝𝑚 ) )
6 bnj545.6 ( ( 𝑅 FrSe 𝐴𝜏𝜎 ) → 𝐺 Fn 𝑛 )
7 bnj545.7 ( 𝜑″ ↔ ( 𝐺 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
8 4 simp1bi ( 𝜏𝑓 Fn 𝑚 )
9 5 simp1bi ( 𝜎𝑚𝐷 )
10 8 9 anim12i ( ( 𝜏𝜎 ) → ( 𝑓 Fn 𝑚𝑚𝐷 ) )
11 10 3adant1 ( ( 𝑅 FrSe 𝐴𝜏𝜎 ) → ( 𝑓 Fn 𝑚𝑚𝐷 ) )
12 2 bnj529 ( 𝑚𝐷 → ∅ ∈ 𝑚 )
13 fndm ( 𝑓 Fn 𝑚 → dom 𝑓 = 𝑚 )
14 eleq2 ( dom 𝑓 = 𝑚 → ( ∅ ∈ dom 𝑓 ↔ ∅ ∈ 𝑚 ) )
15 14 biimparc ( ( ∅ ∈ 𝑚 ∧ dom 𝑓 = 𝑚 ) → ∅ ∈ dom 𝑓 )
16 12 13 15 syl2anr ( ( 𝑓 Fn 𝑚𝑚𝐷 ) → ∅ ∈ dom 𝑓 )
17 11 16 syl ( ( 𝑅 FrSe 𝐴𝜏𝜎 ) → ∅ ∈ dom 𝑓 )
18 6 bnj930 ( ( 𝑅 FrSe 𝐴𝜏𝜎 ) → Fun 𝐺 )
19 17 18 jca ( ( 𝑅 FrSe 𝐴𝜏𝜎 ) → ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺 ) )
20 3 bnj931 𝑓𝐺
21 19 20 jctil ( ( 𝑅 FrSe 𝐴𝜏𝜎 ) → ( 𝑓𝐺 ∧ ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺 ) ) )
22 df-3an ( ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺𝑓𝐺 ) ↔ ( ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺 ) ∧ 𝑓𝐺 ) )
23 3anrot ( ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺𝑓𝐺 ) ↔ ( Fun 𝐺𝑓𝐺 ∧ ∅ ∈ dom 𝑓 ) )
24 ancom ( ( ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺 ) ∧ 𝑓𝐺 ) ↔ ( 𝑓𝐺 ∧ ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺 ) ) )
25 22 23 24 3bitr3i ( ( Fun 𝐺𝑓𝐺 ∧ ∅ ∈ dom 𝑓 ) ↔ ( 𝑓𝐺 ∧ ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺 ) ) )
26 21 25 sylibr ( ( 𝑅 FrSe 𝐴𝜏𝜎 ) → ( Fun 𝐺𝑓𝐺 ∧ ∅ ∈ dom 𝑓 ) )
27 funssfv ( ( Fun 𝐺𝑓𝐺 ∧ ∅ ∈ dom 𝑓 ) → ( 𝐺 ‘ ∅ ) = ( 𝑓 ‘ ∅ ) )
28 26 27 syl ( ( 𝑅 FrSe 𝐴𝜏𝜎 ) → ( 𝐺 ‘ ∅ ) = ( 𝑓 ‘ ∅ ) )
29 4 simp2bi ( 𝜏𝜑′ )
30 29 3ad2ant2 ( ( 𝑅 FrSe 𝐴𝜏𝜎 ) → 𝜑′ )
31 eqtr ( ( ( 𝐺 ‘ ∅ ) = ( 𝑓 ‘ ∅ ) ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) → ( 𝐺 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
32 1 31 sylan2b ( ( ( 𝐺 ‘ ∅ ) = ( 𝑓 ‘ ∅ ) ∧ 𝜑′ ) → ( 𝐺 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
33 32 7 sylibr ( ( ( 𝐺 ‘ ∅ ) = ( 𝑓 ‘ ∅ ) ∧ 𝜑′ ) → 𝜑″ )
34 28 30 33 syl2anc ( ( 𝑅 FrSe 𝐴𝜏𝜎 ) → 𝜑″ )