Metamath Proof Explorer

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 syl5eq ⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) )
42 41 sbceq1d ⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → ( [ 𝐺 / 𝑓 ] 𝜑′ ↔ [ ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) / 𝑓 ] 𝜑′ ) )
43 5 42 syl5bb ⊢ ( 𝐶 = 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 𝑛 ) ) → 𝜑″ )