Metamath Proof Explorer

Theorem bnj600

Description: Technical lemma for bnj852 . 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 bnj600.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
bnj600.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj600.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
bnj600.4 ⊢ ( 𝜒 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
bnj600.5 ⊢ ( 𝜃 ↔ ∀ 𝑚 ∈ 𝐷 ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜒 ) )
bnj600.10 ⊢ ( 𝜑′ ↔ [ 𝑚 / 𝑛 ] 𝜑 )
bnj600.11 ⊢ ( 𝜓′ ↔ [ 𝑚 / 𝑛 ] 𝜓 )
bnj600.12 ⊢ ( 𝜒′ ↔ [ 𝑚 / 𝑛 ] 𝜒 )
bnj600.13 ⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑 )
bnj600.14 ⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓 )
bnj600.15 ⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒 )
bnj600.16 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
bnj600.17 ⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
bnj600.18 ⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
bnj600.19 ⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
bnj600.20 ⊢ ( 𝜁 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖 ) )
bnj600.21 ⊢ ( 𝜌 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) )
bnj600.22 ⊢ 𝐵 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
bnj600.23 ⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
bnj600.24 ⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
bnj600.25 ⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
bnj600.26 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } )
Assertion bnj600 ( 𝑛 ≠ 1o → ( ( 𝑛 ∈ 𝐷 ∧ 𝜃 ) → 𝜒 ) )

Proof

Step Hyp Ref Expression
1 bnj600.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2 bnj600.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj600.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
4 bnj600.4 ⊢ ( 𝜒 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
5 bnj600.5 ⊢ ( 𝜃 ↔ ∀ 𝑚 ∈ 𝐷 ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜒 ) )
6 bnj600.10 ⊢ ( 𝜑′ ↔ [ 𝑚 / 𝑛 ] 𝜑 )
7 bnj600.11 ⊢ ( 𝜓′ ↔ [ 𝑚 / 𝑛 ] 𝜓 )
8 bnj600.12 ⊢ ( 𝜒′ ↔ [ 𝑚 / 𝑛 ] 𝜒 )
9 bnj600.13 ⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑 )
10 bnj600.14 ⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓 )
11 bnj600.15 ⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒 )
12 bnj600.16 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
13 bnj600.17 ⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
14 bnj600.18 ⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
15 bnj600.19 ⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
16 bnj600.20 ⊢ ( 𝜁 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖 ) )
17 bnj600.21 ⊢ ( 𝜌 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) )
18 bnj600.22 ⊢ 𝐵 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
19 bnj600.23 ⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
20 bnj600.24 ⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
21 bnj600.25 ⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
22 bnj600.26 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } )
23 12 bnj528 ⊢ 𝐺 ∈ V
24 vex ⊢ 𝑚 ∈ V
25 4 6 7 8 24 bnj207 ⊢ ( 𝜒′ ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) ) )
26 1 9 23 bnj609 ⊢ ( 𝜑″ ↔ ( 𝐺 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
27 2 10 23 bnj611 ⊢ ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
28 3 bnj168 ⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∈ 𝐷 𝑛 = suc 𝑚 )
29 df-rex ⊢ ( ∃ 𝑚 ∈ 𝐷 𝑛 = suc 𝑚 ↔ ∃ 𝑚 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) )
30 28 29 sylib ⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) )
31 3 bnj158 ⊢ ( 𝑚 ∈ 𝐷 → ∃ 𝑝 ∈ ω 𝑚 = suc 𝑝 )
32 df-rex ⊢ ( ∃ 𝑝 ∈ ω 𝑚 = suc 𝑝 ↔ ∃ 𝑝 ( 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
33 31 32 sylib ⊢ ( 𝑚 ∈ 𝐷 → ∃ 𝑝 ( 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
34 33 adantr ⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) → ∃ 𝑝 ( 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
35 34 ancri ⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) → ( ∃ 𝑝 ( 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) ∧ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) ) )
36 35 bnj534 ⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) → ∃ 𝑝 ( ( 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) ∧ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) ) )
37 bnj432 ⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) ↔ ( ( 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) ∧ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) ) )
38 37 exbii ⊢ ( ∃ 𝑝 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) ↔ ∃ 𝑝 ( ( 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) ∧ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) ) )
39 36 38 sylibr ⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) → ∃ 𝑝 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
40 39 eximi ⊢ ( ∃ 𝑚 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) → ∃ 𝑚 ∃ 𝑝 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
41 30 40 syl ⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∃ 𝑝 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
42 15 2exbii ⊢ ( ∃ 𝑚 ∃ 𝑝 𝜂 ↔ ∃ 𝑚 ∃ 𝑝 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
43 41 42 sylibr ⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∃ 𝑝 𝜂 )
44 rsp ⊢ ( ∀ 𝑚 ∈ 𝐷 ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜒 ) → ( 𝑚 ∈ 𝐷 → ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜒 ) ) )
45 5 44 sylbi ⊢ ( 𝜃 → ( 𝑚 ∈ 𝐷 → ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜒 ) ) )
46 45 3imp ⊢ ( ( 𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) → [ 𝑚 / 𝑛 ] 𝜒 )
47 46 8 sylibr ⊢ ( ( 𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛 ) → 𝜒′ )
48 1 6 24 bnj523 ⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
49 2 7 24 bnj539 ⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
50 48 49 3 12 13 14 bnj544 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐺 Fn 𝑛 )
51 14 15 50 bnj561 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝐺 Fn 𝑛 )
52 48 3 12 13 14 50 26 bnj545 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝜑″ )
53 14 15 52 bnj562 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝜑″ )
54 3 12 13 14 15 16 18 19 20 21 22 48 49 50 17 51 27 bnj571 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝜓″ )
55 biid ⊢ ( [ 𝑧 / 𝑓 ] 𝜑 ↔ [ 𝑧 / 𝑓 ] 𝜑 )
56 biid ⊢ ( [ 𝑧 / 𝑓 ] 𝜓 ↔ [ 𝑧 / 𝑓 ] 𝜓 )
57 biid ⊢ ( [ 𝐺 / 𝑧 ] [ 𝑧 / 𝑓 ] 𝜑 ↔ [ 𝐺 / 𝑧 ] [ 𝑧 / 𝑓 ] 𝜑 )
58 biid ⊢ ( [ 𝐺 / 𝑧 ] [ 𝑧 / 𝑓 ] 𝜓 ↔ [ 𝐺 / 𝑧 ] [ 𝑧 / 𝑓 ] 𝜓 )
59 5 9 10 13 15 23 25 26 27 43 47 51 53 54 1 2 55 56 57 58 bnj607 ⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
60 1 2 3 bnj579 ⊢ ( 𝑛 ∈ 𝐷 → ∃* 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
61 60 a1d ⊢ ( 𝑛 ∈ 𝐷 → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃* 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
62 61 3ad2ant2 ⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃* 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
63 59 62 jcad ⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃* 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) )
64 df-eu ⊢ ( ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃* 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
65 63 64 imbitrrdi ⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
66 65 4 sylibr ⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃 ) → 𝜒 )
67 66 3expib ⊢ ( 𝑛 ≠ 1o → ( ( 𝑛 ∈ 𝐷 ∧ 𝜃 ) → 𝜒 ) )