bnj929

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	bnj929.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
	bnj929.4	⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 )
	bnj929.7	⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ )
	bnj929.10	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj929.13	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
	bnj929.50	⊢ 𝐶 ∈ V
Assertion	bnj929	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) → 𝜑″ )

Proof

Step	Hyp	Ref	Expression
1		bnj929.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2		bnj929.4	⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 )
3		bnj929.7	⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ )
4		bnj929.10	⊢ 𝐷 = ( ω ∖ { ∅ } )
5		bnj929.13	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
6		bnj929.50	⊢ 𝐶 ∈ V
7		bnj645	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) → 𝜑 )
8		bnj334	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) ↔ ( 𝑓 Fn 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝜑 ) )
9		bnj257	⊢ ( ( 𝑓 Fn 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝜑 ) ↔ ( 𝑓 Fn 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜑 ∧ 𝑝 = suc 𝑛 ) )
10	8 9	bitri	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) ↔ ( 𝑓 Fn 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜑 ∧ 𝑝 = suc 𝑛 ) )
11		bnj345	⊢ ( ( 𝑓 Fn 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜑 ∧ 𝑝 = suc 𝑛 ) ↔ ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜑 ) )
12		bnj253	⊢ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜑 ) ↔ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) ∧ 𝑛 ∈ 𝐷 ∧ 𝜑 ) )
13	10 11 12	3bitri	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) ↔ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) ∧ 𝑛 ∈ 𝐷 ∧ 𝜑 ) )
14	13	simp1bi	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) → ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) )
15	5 6	bnj927	⊢ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → 𝐺 Fn 𝑝 )
16	15	fnfund	⊢ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → Fun 𝐺 )
17	14 16	syl	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) → Fun 𝐺 )
18	5	bnj931	⊢ 𝑓 ⊆ 𝐺
19	18	a1i	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) → 𝑓 ⊆ 𝐺 )
20		bnj268	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝜑 ) ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) )
21		bnj253	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝜑 ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ) ∧ 𝑝 = suc 𝑛 ∧ 𝜑 ) )
22	20 21	bitr3i	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ) ∧ 𝑝 = suc 𝑛 ∧ 𝜑 ) )
23	22	simp1bi	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) → ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ) )
24		fndm	⊢ ( 𝑓 Fn 𝑛 → dom 𝑓 = 𝑛 )
25	4	bnj529	⊢ ( 𝑛 ∈ 𝐷 → ∅ ∈ 𝑛 )
26		eleq2	⊢ ( dom 𝑓 = 𝑛 → ( ∅ ∈ dom 𝑓 ↔ ∅ ∈ 𝑛 ) )
27	26	biimpar	⊢ ( ( dom 𝑓 = 𝑛 ∧ ∅ ∈ 𝑛 ) → ∅ ∈ dom 𝑓 )
28	24 25 27	syl2anr	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ) → ∅ ∈ dom 𝑓 )
29	23 28	syl	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) → ∅ ∈ dom 𝑓 )
30	17 19 29	bnj1502	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) → ( 𝐺 ‘ ∅ ) = ( 𝑓 ‘ ∅ ) )
31	5	bnj918	⊢ 𝐺 ∈ V
32	1 2 3 31	bnj934	⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ ∅ ) = ( 𝑓 ‘ ∅ ) ) → 𝜑″ )
33	7 30 32	syl2anc	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) → 𝜑″ )

Metamath Proof Explorer

Theorem bnj929

Proof