Theorem bnj910

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	bnj910.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
	bnj910.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj910.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
	bnj910.4	⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 )
	bnj910.5	⊢ ( 𝜓′ ↔ [ 𝑝 / 𝑛 ] 𝜓 )
	bnj910.6	⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 )
	bnj910.7	⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ )
	bnj910.8	⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓′ )
	bnj910.9	⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ )
	bnj910.10	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj910.11	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
	bnj910.12	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj910.13	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
	bnj910.14	⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
	bnj910.15	⊢ ( 𝜎 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛 ) )
Assertion	bnj910	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝜒″ )

Proof

Step	Hyp	Ref	Expression
1		bnj910.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2		bnj910.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj910.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
4		bnj910.4	⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 )
5		bnj910.5	⊢ ( 𝜓′ ↔ [ 𝑝 / 𝑛 ] 𝜓 )
6		bnj910.6	⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 )
7		bnj910.7	⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ )
8		bnj910.8	⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓′ )
9		bnj910.9	⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ )
10		bnj910.10	⊢ 𝐷 = ( ω ∖ { ∅ } )
11		bnj910.11	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
12		bnj910.12	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
13		bnj910.13	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
14		bnj910.14	⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
15		bnj910.15	⊢ ( 𝜎 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛 ) )
16	3 10	bnj970	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝑝 ∈ 𝐷 )
17	1 2 3 10 12 14 15	bnj969	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝐶 ∈ V )
18		simpr3	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝑝 = suc 𝑛 )
19	3	bnj1235	⊢ ( 𝜒 → 𝑓 Fn 𝑛 )
20	19	3ad2ant1	⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → 𝑓 Fn 𝑛 )
21	20	adantl	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝑓 Fn 𝑛 )
22	13	bnj941	⊢ ( 𝐶 ∈ V → ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → 𝐺 Fn 𝑝 ) )
23	22	3impib	⊢ ( ( 𝐶 ∈ V ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → 𝐺 Fn 𝑝 )
24	17 18 21 23	syl3anc	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝐺 Fn 𝑝 )
25	1 2 3 4 7 10 12 13 14 15	bnj944	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝜑″ )
26	2 3 10 12 13 17	bnj967	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
27	3 10 12 13 17 24	bnj966	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
28	2 3 5 8 12 13 26 27	bnj964	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝜓″ )
29	16 24 25 28	bnj951	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → ( 𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″ ) )
30		vex	⊢ 𝑝 ∈ V
31	3 4 5 6 30	bnj919	⊢ ( 𝜒′ ↔ ( 𝑝 ∈ 𝐷 ∧ 𝑓 Fn 𝑝 ∧ 𝜑′ ∧ 𝜓′ ) )
32	13	bnj918	⊢ 𝐺 ∈ V
33	31 7 8 9 32	bnj976	⊢ ( 𝜒″ ↔ ( 𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″ ) )
34	29 33	sylibr	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝜒″ )