Mathbox for Jonathan Ben-Naim < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj607 Structured version   Visualization version   GIF version

Theorem bnj607 32298
 Description: Technical lemma for bnj852 32303. 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.)
Hypotheses
Ref Expression
bnj607.5 (𝜃 ↔ ∀𝑚𝐷 (𝑚 E 𝑛[𝑚 / 𝑛]𝜒))
bnj607.13 (𝜑″[𝐺 / 𝑓]𝜑)
bnj607.14 (𝜓″[𝐺 / 𝑓]𝜓)
bnj607.17 (𝜏 ↔ (𝑓 Fn 𝑚𝜑′𝜓′))
bnj607.19 (𝜂 ↔ (𝑚𝐷𝑛 = suc 𝑚𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))
bnj607.28 𝐺 ∈ V
bnj607.31 (𝜒′ ↔ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
bnj607.32 (𝜑″ ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅))
bnj607.33 (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝐺‘suc 𝑖) = 𝑦 ∈ (𝐺𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj607.37 ((𝑛 ≠ 1o𝑛𝐷) → ∃𝑚𝑝𝜂)
bnj607.38 ((𝜃𝑚𝐷𝑚 E 𝑛) → 𝜒′)
bnj607.41 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝐺 Fn 𝑛)
bnj607.42 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜑″)
bnj607.43 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜓″)
bnj607.1 (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
bnj607.2 (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj607.400 (𝜑0[ / 𝑓]𝜑)
bnj607.401 (𝜓0[ / 𝑓]𝜓)
bnj607.300 (𝜑1[𝐺 / ]𝜑0)
bnj607.301 (𝜓1[𝐺 / ]𝜓0)
Assertion
Ref Expression
bnj607 ((𝑛 ≠ 1o𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
Distinct variable groups:   𝐴,𝑓,   𝐴,𝑚,𝑓   𝐴,𝑝,𝑓   ,𝐺,𝑖,𝑦   𝑅,𝑓,   𝑅,𝑚   𝑅,𝑝   𝜂,𝑓   𝑓,𝑖,𝑦   𝑓,𝑛,   𝑥,𝑓,   𝜑,   𝜓,   𝑚,𝑛   𝜑,𝑚   𝜓,𝑚   𝑥,𝑚   𝑛,𝑝   𝜑,𝑝   𝜓,𝑝   𝜃,𝑝   𝑥,𝑝
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓,𝑖,𝑛)   𝜓(𝑥,𝑦,𝑓,𝑖,𝑛)   𝜒(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜃(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛)   𝜏(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜂(𝑥,𝑦,,𝑖,𝑚,𝑛,𝑝)   𝐴(𝑥,𝑦,𝑖,𝑛)   𝐷(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝑅(𝑥,𝑦,𝑖,𝑛)   𝐺(𝑥,𝑓,𝑚,𝑛,𝑝)   𝜑′(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜓′(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜒′(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜑″(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜓″(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜑0(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜓0(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜑1(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜓1(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)

Proof of Theorem bnj607
StepHypRef Expression
1 bnj607.37 . . . . 5 ((𝑛 ≠ 1o𝑛𝐷) → ∃𝑚𝑝𝜂)
21anim1i 617 . . . 4 (((𝑛 ≠ 1o𝑛𝐷) ∧ 𝜃) → (∃𝑚𝑝𝜂𝜃))
3 nfv 1915 . . . . . . 7 𝑝𝜃
4319.41 2235 . . . . . 6 (∃𝑝(𝜂𝜃) ↔ (∃𝑝𝜂𝜃))
54exbii 1849 . . . . 5 (∃𝑚𝑝(𝜂𝜃) ↔ ∃𝑚(∃𝑝𝜂𝜃))
6 bnj607.5 . . . . . . . 8 (𝜃 ↔ ∀𝑚𝐷 (𝑚 E 𝑛[𝑚 / 𝑛]𝜒))
76bnj1095 32163 . . . . . . 7 (𝜃 → ∀𝑚𝜃)
87nf5i 2147 . . . . . 6 𝑚𝜃
9819.41 2235 . . . . 5 (∃𝑚(∃𝑝𝜂𝜃) ↔ (∃𝑚𝑝𝜂𝜃))
105, 9bitr2i 279 . . . 4 ((∃𝑚𝑝𝜂𝜃) ↔ ∃𝑚𝑝(𝜂𝜃))
112, 10sylib 221 . . 3 (((𝑛 ≠ 1o𝑛𝐷) ∧ 𝜃) → ∃𝑚𝑝(𝜂𝜃))
12 bnj607.19 . . . . . . . . . 10 (𝜂 ↔ (𝑚𝐷𝑛 = suc 𝑚𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))
1312bnj1232 32185 . . . . . . . . 9 (𝜂𝑚𝐷)
14 bnj219 32113 . . . . . . . . . 10 (𝑛 = suc 𝑚𝑚 E 𝑛)
1512, 14bnj770 32144 . . . . . . . . 9 (𝜂𝑚 E 𝑛)
1613, 15jca 515 . . . . . . . 8 (𝜂 → (𝑚𝐷𝑚 E 𝑛))
1716anim1i 617 . . . . . . 7 ((𝜂𝜃) → ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
18 bnj170 32078 . . . . . . 7 ((𝜃𝑚𝐷𝑚 E 𝑛) ↔ ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
1917, 18sylibr 237 . . . . . 6 ((𝜂𝜃) → (𝜃𝑚𝐷𝑚 E 𝑛))
20 bnj607.38 . . . . . 6 ((𝜃𝑚𝐷𝑚 E 𝑛) → 𝜒′)
2119, 20syl 17 . . . . 5 ((𝜂𝜃) → 𝜒′)
22 simpl 486 . . . . 5 ((𝜂𝜃) → 𝜂)
2321, 22jca 515 . . . 4 ((𝜂𝜃) → (𝜒′𝜂))
24232eximi 1837 . . 3 (∃𝑚𝑝(𝜂𝜃) → ∃𝑚𝑝(𝜒′𝜂))
25 bnj607.31 . . . . . . . . . . . 12 (𝜒′ ↔ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
2625biimpi 219 . . . . . . . . . . 11 (𝜒′ → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
27 euex 2637 . . . . . . . . . . 11 (∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
2826, 27syl6 35 . . . . . . . . . 10 (𝜒′ → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
2928impcom 411 . . . . . . . . 9 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
30 bnj607.17 . . . . . . . . 9 (𝜏 ↔ (𝑓 Fn 𝑚𝜑′𝜓′))
3129, 30bnj1198 32177 . . . . . . . 8 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓𝜏)
3231adantrr 716 . . . . . . 7 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ (𝜒′𝜂)) → ∃𝑓𝜏)
33 id 22 . . . . . . . . . . 11 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝑅 FrSe 𝐴𝜏𝜂))
34333com23 1123 . . . . . . . . . 10 ((𝑅 FrSe 𝐴𝜂𝜏) → (𝑅 FrSe 𝐴𝜏𝜂))
35343expia 1118 . . . . . . . . 9 ((𝑅 FrSe 𝐴𝜂) → (𝜏 → (𝑅 FrSe 𝐴𝜏𝜂)))
3635eximdv 1918 . . . . . . . 8 ((𝑅 FrSe 𝐴𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑅 FrSe 𝐴𝜏𝜂)))
3736ad2ant2rl 748 . . . . . . 7 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ (𝜒′𝜂)) → (∃𝑓𝜏 → ∃𝑓(𝑅 FrSe 𝐴𝜏𝜂)))
3832, 37mpd 15 . . . . . 6 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ (𝜒′𝜂)) → ∃𝑓(𝑅 FrSe 𝐴𝜏𝜂))
39 bnj607.41 . . . . . . . 8 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝐺 Fn 𝑛)
40 bnj607.42 . . . . . . . 8 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜑″)
41 bnj607.43 . . . . . . . 8 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜓″)
4239, 40, 413jca 1125 . . . . . . 7 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝐺 Fn 𝑛𝜑″𝜓″))
4342eximi 1836 . . . . . 6 (∃𝑓(𝑅 FrSe 𝐴𝜏𝜂) → ∃𝑓(𝐺 Fn 𝑛𝜑″𝜓″))
44 nfe1 2151 . . . . . . 7 𝑓𝑓(𝑓 Fn 𝑛𝜑𝜓)
45 bnj607.28 . . . . . . . . 9 𝐺 ∈ V
46 nfcv 2955 . . . . . . . . . 10 𝐺
47 nfv 1915 . . . . . . . . . . 11 𝐺 Fn 𝑛
48 bnj607.300 . . . . . . . . . . . 12 (𝜑1[𝐺 / ]𝜑0)
49 nfsbc1v 3740 . . . . . . . . . . . 12 [𝐺 / ]𝜑0
5048, 49nfxfr 1854 . . . . . . . . . . 11 𝜑1
51 bnj607.301 . . . . . . . . . . . 12 (𝜓1[𝐺 / ]𝜓0)
52 nfsbc1v 3740 . . . . . . . . . . . 12 [𝐺 / ]𝜓0
5351, 52nfxfr 1854 . . . . . . . . . . 11 𝜓1
5447, 50, 53nf3an 1902 . . . . . . . . . 10 (𝐺 Fn 𝑛𝜑1𝜓1)
55 fneq1 6414 . . . . . . . . . . 11 ( = 𝐺 → ( Fn 𝑛𝐺 Fn 𝑛))
56 sbceq1a 3731 . . . . . . . . . . . 12 ( = 𝐺 → (𝜑0[𝐺 / ]𝜑0))
5756, 48syl6bbr 292 . . . . . . . . . . 11 ( = 𝐺 → (𝜑0𝜑1))
58 sbceq1a 3731 . . . . . . . . . . . 12 ( = 𝐺 → (𝜓0[𝐺 / ]𝜓0))
5958, 51syl6bbr 292 . . . . . . . . . . 11 ( = 𝐺 → (𝜓0𝜓1))
6055, 57, 593anbi123d 1433 . . . . . . . . . 10 ( = 𝐺 → (( Fn 𝑛𝜑0𝜓0) ↔ (𝐺 Fn 𝑛𝜑1𝜓1)))
6146, 54, 60spcegf 3539 . . . . . . . . 9 (𝐺 ∈ V → ((𝐺 Fn 𝑛𝜑1𝜓1) → ∃( Fn 𝑛𝜑0𝜓0)))
6245, 61ax-mp 5 . . . . . . . 8 ((𝐺 Fn 𝑛𝜑1𝜓1) → ∃( Fn 𝑛𝜑0𝜓0))
63 bnj607.32 . . . . . . . . . . . 12 (𝜑″ ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅))
64 bnj607.400 . . . . . . . . . . . . . 14 (𝜑0[ / 𝑓]𝜑)
65 bnj607.1 . . . . . . . . . . . . . 14 (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
6664, 65bnj154 32260 . . . . . . . . . . . . 13 (𝜑0 ↔ (‘∅) = pred(𝑥, 𝐴, 𝑅))
6766, 48, 45bnj526 32270 . . . . . . . . . . . 12 (𝜑1 ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅))
6863, 67bitr4i 281 . . . . . . . . . . 11 (𝜑″𝜑1)
69 bnj607.33 . . . . . . . . . . . 12 (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝐺‘suc 𝑖) = 𝑦 ∈ (𝐺𝑖) pred(𝑦, 𝐴, 𝑅)))
70 bnj607.2 . . . . . . . . . . . . . 14 (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
71 bnj607.401 . . . . . . . . . . . . . 14 (𝜓0[ / 𝑓]𝜓)
72 vex 3444 . . . . . . . . . . . . . 14 ∈ V
7370, 71, 72bnj540 32274 . . . . . . . . . . . . 13 (𝜓0 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (‘suc 𝑖) = 𝑦 ∈ (𝑖) pred(𝑦, 𝐴, 𝑅)))
7473, 51, 45bnj540 32274 . . . . . . . . . . . 12 (𝜓1 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝐺‘suc 𝑖) = 𝑦 ∈ (𝐺𝑖) pred(𝑦, 𝐴, 𝑅)))
7569, 74bitr4i 281 . . . . . . . . . . 11 (𝜓″𝜓1)
7668, 75anbi12i 629 . . . . . . . . . 10 ((𝜑″𝜓″) ↔ (𝜑1𝜓1))
7776anbi2i 625 . . . . . . . . 9 ((𝐺 Fn 𝑛 ∧ (𝜑″𝜓″)) ↔ (𝐺 Fn 𝑛 ∧ (𝜑1𝜓1)))
78 3anass 1092 . . . . . . . . 9 ((𝐺 Fn 𝑛𝜑″𝜓″) ↔ (𝐺 Fn 𝑛 ∧ (𝜑″𝜓″)))
79 3anass 1092 . . . . . . . . 9 ((𝐺 Fn 𝑛𝜑1𝜓1) ↔ (𝐺 Fn 𝑛 ∧ (𝜑1𝜓1)))
8077, 78, 793bitr4i 306 . . . . . . . 8 ((𝐺 Fn 𝑛𝜑″𝜓″) ↔ (𝐺 Fn 𝑛𝜑1𝜓1))
81 nfv 1915 . . . . . . . . 9 (𝑓 Fn 𝑛𝜑𝜓)
82 nfv 1915 . . . . . . . . . 10 𝑓 Fn 𝑛
83 nfsbc1v 3740 . . . . . . . . . . 11 𝑓[ / 𝑓]𝜑
8464, 83nfxfr 1854 . . . . . . . . . 10 𝑓𝜑0
85 nfsbc1v 3740 . . . . . . . . . . 11 𝑓[ / 𝑓]𝜓
8671, 85nfxfr 1854 . . . . . . . . . 10 𝑓𝜓0
8782, 84, 86nf3an 1902 . . . . . . . . 9 𝑓( Fn 𝑛𝜑0𝜓0)
88 fneq1 6414 . . . . . . . . . 10 (𝑓 = → (𝑓 Fn 𝑛 Fn 𝑛))
89 sbceq1a 3731 . . . . . . . . . . 11 (𝑓 = → (𝜑[ / 𝑓]𝜑))
9089, 64syl6bbr 292 . . . . . . . . . 10 (𝑓 = → (𝜑𝜑0))
91 sbceq1a 3731 . . . . . . . . . . 11 (𝑓 = → (𝜓[ / 𝑓]𝜓))
9291, 71syl6bbr 292 . . . . . . . . . 10 (𝑓 = → (𝜓𝜓0))
9388, 90, 923anbi123d 1433 . . . . . . . . 9 (𝑓 = → ((𝑓 Fn 𝑛𝜑𝜓) ↔ ( Fn 𝑛𝜑0𝜓0)))
9481, 87, 93cbvexv1 2351 . . . . . . . 8 (∃𝑓(𝑓 Fn 𝑛𝜑𝜓) ↔ ∃( Fn 𝑛𝜑0𝜓0))
9562, 80, 943imtr4i 295 . . . . . . 7 ((𝐺 Fn 𝑛𝜑″𝜓″) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9644, 95exlimi 2215 . . . . . 6 (∃𝑓(𝐺 Fn 𝑛𝜑″𝜓″) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9738, 43, 963syl 18 . . . . 5 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ (𝜒′𝜂)) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9897expcom 417 . . . 4 ((𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
9998exlimivv 1933 . . 3 (∃𝑚𝑝(𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
10011, 24, 993syl 18 . 2 (((𝑛 ≠ 1o𝑛𝐷) ∧ 𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
1011003impa 1107 1 ((𝑛 ≠ 1o𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∃!weu 2628   ≠ wne 2987  ∀wral 3106  Vcvv 3441  [wsbc 3720  ∅c0 4243  ∪ ciun 4881   class class class wbr 5030   E cep 5429  suc csuc 6161   Fn wfn 6319  ‘cfv 6324  ωcom 7560  1oc1o 8078   ∧ w-bnj17 32066   predc-bnj14 32068   FrSe w-bnj15 32072 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-eprel 5430  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-fv 6332  df-bnj17 32067 This theorem is referenced by:  bnj600  32301
 Copyright terms: Public domain W3C validator