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

Metamath Proof Explorer

Theorem bnj545

Proof