Theorem bnj944

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

Proof

Step	Hyp	Ref	Expression
1		bnj944.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2		bnj944.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj944.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
4		bnj944.4	⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 )
5		bnj944.7	⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ )
6		bnj944.10	⊢ 𝐷 = ( ω ∖ { ∅ } )
7		bnj944.12	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
8		bnj944.13	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
9		bnj944.14	⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
10		bnj944.15	⊢ ( 𝜎 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛 ) )
11		simpl	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
12		bnj667	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
13	3 12	sylbi	⊢ ( 𝜒 → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
14	13 9	sylibr	⊢ ( 𝜒 → 𝜏 )
15	14	3ad2ant1	⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → 𝜏 )
16	15	adantl	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝜏 )
17	3	bnj1232	⊢ ( 𝜒 → 𝑛 ∈ 𝐷 )
18		vex	⊢ 𝑚 ∈ V
19	18	bnj216	⊢ ( 𝑛 = suc 𝑚 → 𝑚 ∈ 𝑛 )
20		id	⊢ ( 𝑝 = suc 𝑛 → 𝑝 = suc 𝑛 )
21	17 19 20	3anim123i	⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → ( 𝑛 ∈ 𝐷 ∧ 𝑚 ∈ 𝑛 ∧ 𝑝 = suc 𝑛 ) )
22		3ancomb	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛 ) ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑚 ∈ 𝑛 ∧ 𝑝 = suc 𝑛 ) )
23	10 22	bitri	⊢ ( 𝜎 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑚 ∈ 𝑛 ∧ 𝑝 = suc 𝑛 ) )
24	21 23	sylibr	⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → 𝜎 )
25	24	adantl	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝜎 )
26		bnj253	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝜏 ∧ 𝜎 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝜏 ∧ 𝜎 ) )
27	11 16 25 26	syl3anbrc	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝜏 ∧ 𝜎 ) )
28	6 9 10 1 2	bnj938	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝜏 ∧ 𝜎 ) → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
29	7 28	eqeltrid	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐶 ∈ V )
30	27 29	syl	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝐶 ∈ V )
31		bnj658	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) → ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) )
32	3 31	sylbi	⊢ ( 𝜒 → ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) )
33	32	3ad2ant1	⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) )
34		simp3	⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → 𝑝 = suc 𝑛 )
35		bnj291	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) ∧ 𝑝 = suc 𝑛 ) )
36	33 34 35	sylanbrc	⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) )
37	36	adantl	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) )
38		opeq2	⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → ⟨ 𝑛 , 𝐶 ⟩ = ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ )
39	38	sneqd	⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → { ⟨ 𝑛 , 𝐶 ⟩ } = { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } )
40	39	uneq2d	⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } ) = ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) )
41	8 40	eqtrid	⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) )
42	41	sbceq1d	⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → ( [ 𝐺 / 𝑓 ] 𝜑′ ↔ [ ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) / 𝑓 ] 𝜑′ ) )
43	5 42	bitrid	⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → ( 𝜑″ ↔ [ ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) / 𝑓 ] 𝜑′ ) )
44	43	imbi2d	⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → ( ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) → 𝜑″ ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) → [ ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) / 𝑓 ] 𝜑′ ) ) )
45		biid	⊢ ( [ ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) / 𝑓 ] 𝜑′ ↔ [ ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) / 𝑓 ] 𝜑′ )
46		eqid	⊢ ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) = ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } )
47		0ex	⊢ ∅ ∈ V
48	47	elimel	⊢ if ( 𝐶 ∈ V , 𝐶 , ∅ ) ∈ V
49	1 4 45 6 46 48	bnj929	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) → [ ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) / 𝑓 ] 𝜑′ )
50	44 49	dedth	⊢ ( 𝐶 ∈ V → ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ) → 𝜑″ ) )
51	30 37 50	sylc	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝜑″ )