This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 fnfund ⊢ ( ( 𝑅 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 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝜑″ )