Metamath Proof Explorer


Theorem bnj969

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 bnj969.1 ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
bnj969.2 ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj969.3 ( 𝜒 ↔ ( 𝑛𝐷𝑓 Fn 𝑛𝜑𝜓 ) )
bnj969.10 𝐷 = ( ω ∖ { ∅ } )
bnj969.12 𝐶 = 𝑦 ∈ ( 𝑓𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
bnj969.14 ( 𝜏 ↔ ( 𝑓 Fn 𝑛𝜑𝜓 ) )
bnj969.15 ( 𝜎 ↔ ( 𝑛𝐷𝑝 = suc 𝑛𝑚𝑛 ) )
Assertion bnj969 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝐶 ∈ V )

Proof

Step Hyp Ref Expression
1 bnj969.1 ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2 bnj969.2 ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj969.3 ( 𝜒 ↔ ( 𝑛𝐷𝑓 Fn 𝑛𝜑𝜓 ) )
4 bnj969.10 𝐷 = ( ω ∖ { ∅ } )
5 bnj969.12 𝐶 = 𝑦 ∈ ( 𝑓𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
6 bnj969.14 ( 𝜏 ↔ ( 𝑓 Fn 𝑛𝜑𝜓 ) )
7 bnj969.15 ( 𝜎 ↔ ( 𝑛𝐷𝑝 = suc 𝑛𝑚𝑛 ) )
8 simpl ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → ( 𝑅 FrSe 𝐴𝑋𝐴 ) )
9 bnj667 ( ( 𝑛𝐷𝑓 Fn 𝑛𝜑𝜓 ) → ( 𝑓 Fn 𝑛𝜑𝜓 ) )
10 9 3 6 3imtr4i ( 𝜒𝜏 )
11 10 3ad2ant1 ( ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) → 𝜏 )
12 11 adantl ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝜏 )
13 3 bnj1232 ( 𝜒𝑛𝐷 )
14 vex 𝑚 ∈ V
15 14 bnj216 ( 𝑛 = suc 𝑚𝑚𝑛 )
16 id ( 𝑝 = suc 𝑛𝑝 = suc 𝑛 )
17 13 15 16 3anim123i ( ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) → ( 𝑛𝐷𝑚𝑛𝑝 = suc 𝑛 ) )
18 3ancomb ( ( 𝑛𝐷𝑝 = suc 𝑛𝑚𝑛 ) ↔ ( 𝑛𝐷𝑚𝑛𝑝 = suc 𝑛 ) )
19 7 18 bitri ( 𝜎 ↔ ( 𝑛𝐷𝑚𝑛𝑝 = suc 𝑛 ) )
20 17 19 sylibr ( ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) → 𝜎 )
21 20 adantl ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝜎 )
22 8 12 21 jca32 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜏𝜎 ) ) )
23 bnj256 ( ( 𝑅 FrSe 𝐴𝑋𝐴𝜏𝜎 ) ↔ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜏𝜎 ) ) )
24 22 23 sylibr ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → ( 𝑅 FrSe 𝐴𝑋𝐴𝜏𝜎 ) )
25 4 6 7 1 2 bnj938 ( ( 𝑅 FrSe 𝐴𝑋𝐴𝜏𝜎 ) → 𝑦 ∈ ( 𝑓𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
26 5 25 eqeltrid ( ( 𝑅 FrSe 𝐴𝑋𝐴𝜏𝜎 ) → 𝐶 ∈ V )
27 24 26 syl ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝐶 ∈ V )