Metamath Proof Explorer

Theorem bnj580

Description: Technical lemma for bnj579 . 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 bnj580.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
bnj580.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj580.3 ⊢ ( 𝜒 ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
bnj580.4 ⊢ ( 𝜑′ ↔ [ 𝑔 / 𝑓 ] 𝜑 )
bnj580.5 ⊢ ( 𝜓′ ↔ [ 𝑔 / 𝑓 ] 𝜓 )
bnj580.6 ⊢ ( 𝜒′ ↔ [ 𝑔 / 𝑓 ] 𝜒 )
bnj580.7 ⊢ 𝐷 = ( ω ∖ { ∅ } )
bnj580.8 ⊢ ( 𝜃 ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
bnj580.9 ⊢ ( 𝜏 ↔ ∀ 𝑘 ∈ 𝑛 ( 𝑘 E 𝑗 → [ 𝑘 / 𝑗 ] 𝜃 ) )
Assertion bnj580 ( 𝑛 ∈ 𝐷 → ∃* 𝑓 𝜒 )

Proof

Step Hyp Ref Expression
1 bnj580.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2 bnj580.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj580.3 ⊢ ( 𝜒 ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
4 bnj580.4 ⊢ ( 𝜑′ ↔ [ 𝑔 / 𝑓 ] 𝜑 )
5 bnj580.5 ⊢ ( 𝜓′ ↔ [ 𝑔 / 𝑓 ] 𝜓 )
6 bnj580.6 ⊢ ( 𝜒′ ↔ [ 𝑔 / 𝑓 ] 𝜒 )
7 bnj580.7 ⊢ 𝐷 = ( ω ∖ { ∅ } )
8 bnj580.8 ⊢ ( 𝜃 ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
9 bnj580.9 ⊢ ( 𝜏 ↔ ∀ 𝑘 ∈ 𝑛 ( 𝑘 E 𝑗 → [ 𝑘 / 𝑗 ] 𝜃 ) )
10 3 simp1bi ⊢ ( 𝜒 → 𝑓 Fn 𝑛 )
11 3 4 5 6 bnj581 ⊢ ( 𝜒′ ↔ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) )
12 11 simp1bi ⊢ ( 𝜒′ → 𝑔 Fn 𝑛 )
13 10 12 bnj240 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 Fn 𝑛 ∧ 𝑔 Fn 𝑛 ) )
14 4 1 bnj154 ⊢ ( 𝜑′ ↔ ( 𝑔 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
15 vex ⊢ 𝑔 ∈ V
16 2 5 15 bnj540 ⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑔 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
17 8 bnj591 ⊢ ( [ 𝑘 / 𝑗 ] 𝜃 ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) ) )
18 1 2 3 7 14 16 11 8 17 9 bnj594 ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝜏 ) → 𝜃 )
19 18 ex ⊢ ( 𝑗 ∈ 𝑛 → ( 𝜏 → 𝜃 ) )
20 19 rgen ⊢ ∀ 𝑗 ∈ 𝑛 ( 𝜏 → 𝜃 )
21 vex ⊢ 𝑛 ∈ V
22 21 9 bnj110 ⊢ ( ( E Fr 𝑛 ∧ ∀ 𝑗 ∈ 𝑛 ( 𝜏 → 𝜃 ) ) → ∀ 𝑗 ∈ 𝑛 𝜃 )
23 20 22 mpan2 ⊢ ( E Fr 𝑛 → ∀ 𝑗 ∈ 𝑛 𝜃 )
24 8 ralbii ⊢ ( ∀ 𝑗 ∈ 𝑛 𝜃 ↔ ∀ 𝑗 ∈ 𝑛 ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
25 23 24 sylib ⊢ ( E Fr 𝑛 → ∀ 𝑗 ∈ 𝑛 ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
26 25 r19.21be ⊢ ∀ 𝑗 ∈ 𝑛 ( E Fr 𝑛 → ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
27 7 bnj923 ⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω )
28 nnord ⊢ ( 𝑛 ∈ ω → Ord 𝑛 )
29 ordfr ⊢ ( Ord 𝑛 → E Fr 𝑛 )
30 27 28 29 3syl ⊢ ( 𝑛 ∈ 𝐷 → E Fr 𝑛 )
31 30 3ad2ant1 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → E Fr 𝑛 )
32 31 pm4.71ri ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ↔ ( E Fr 𝑛 ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) )
33 32 imbi1i ⊢ ( ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) ↔ ( ( E Fr 𝑛 ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
34 impexp ⊢ ( ( ( E Fr 𝑛 ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) ↔ ( E Fr 𝑛 → ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) ) )
35 33 34 bitri ⊢ ( ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) ↔ ( E Fr 𝑛 → ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) ) )
36 35 ralbii ⊢ ( ∀ 𝑗 ∈ 𝑛 ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ 𝑛 ( E Fr 𝑛 → ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) ) )
37 26 36 mpbir ⊢ ∀ 𝑗 ∈ 𝑛 ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) )
38 r19.21v ⊢ ( ∀ 𝑗 ∈ 𝑛 ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ∀ 𝑗 ∈ 𝑛 ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
39 37 38 mpbi ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ∀ 𝑗 ∈ 𝑛 ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) )
40 eqfnfv ⊢ ( ( 𝑓 Fn 𝑛 ∧ 𝑔 Fn 𝑛 ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑗 ∈ 𝑛 ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
41 40 biimprd ⊢ ( ( 𝑓 Fn 𝑛 ∧ 𝑔 Fn 𝑛 ) → ( ∀ 𝑗 ∈ 𝑛 ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) → 𝑓 = 𝑔 ) )
42 13 39 41 sylc ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → 𝑓 = 𝑔 )
43 42 3expib ⊢ ( 𝑛 ∈ 𝐷 → ( ( 𝜒 ∧ 𝜒′ ) → 𝑓 = 𝑔 ) )
44 43 alrimivv ⊢ ( 𝑛 ∈ 𝐷 → ∀ 𝑓 ∀ 𝑔 ( ( 𝜒 ∧ 𝜒′ ) → 𝑓 = 𝑔 ) )
45 sbsbc ⊢ ( [ 𝑔 / 𝑓 ] 𝜒 ↔ [ 𝑔 / 𝑓 ] 𝜒 )
46 45 anbi2i ⊢ ( ( 𝜒 ∧ [ 𝑔 / 𝑓 ] 𝜒 ) ↔ ( 𝜒 ∧ [ 𝑔 / 𝑓 ] 𝜒 ) )
47 46 imbi1i ⊢ ( ( ( 𝜒 ∧ [ 𝑔 / 𝑓 ] 𝜒 ) → 𝑓 = 𝑔 ) ↔ ( ( 𝜒 ∧ [ 𝑔 / 𝑓 ] 𝜒 ) → 𝑓 = 𝑔 ) )
48 47 2albii ⊢ ( ∀ 𝑓 ∀ 𝑔 ( ( 𝜒 ∧ [ 𝑔 / 𝑓 ] 𝜒 ) → 𝑓 = 𝑔 ) ↔ ∀ 𝑓 ∀ 𝑔 ( ( 𝜒 ∧ [ 𝑔 / 𝑓 ] 𝜒 ) → 𝑓 = 𝑔 ) )
49 nfv ⊢ Ⅎ 𝑔 𝜒
50 49 mo3 ⊢ ( ∃* 𝑓 𝜒 ↔ ∀ 𝑓 ∀ 𝑔 ( ( 𝜒 ∧ [ 𝑔 / 𝑓 ] 𝜒 ) → 𝑓 = 𝑔 ) )
51 6 anbi2i ⊢ ( ( 𝜒 ∧ 𝜒′ ) ↔ ( 𝜒 ∧ [ 𝑔 / 𝑓 ] 𝜒 ) )
52 51 imbi1i ⊢ ( ( ( 𝜒 ∧ 𝜒′ ) → 𝑓 = 𝑔 ) ↔ ( ( 𝜒 ∧ [ 𝑔 / 𝑓 ] 𝜒 ) → 𝑓 = 𝑔 ) )
53 52 2albii ⊢ ( ∀ 𝑓 ∀ 𝑔 ( ( 𝜒 ∧ 𝜒′ ) → 𝑓 = 𝑔 ) ↔ ∀ 𝑓 ∀ 𝑔 ( ( 𝜒 ∧ [ 𝑔 / 𝑓 ] 𝜒 ) → 𝑓 = 𝑔 ) )
54 48 50 53 3bitr4i ⊢ ( ∃* 𝑓 𝜒 ↔ ∀ 𝑓 ∀ 𝑔 ( ( 𝜒 ∧ 𝜒′ ) → 𝑓 = 𝑔 ) )
55 44 54 sylibr ⊢ ( 𝑛 ∈ 𝐷 → ∃* 𝑓 𝜒 )