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 30240
 Description: Technical lemma for bnj852 30245. 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 ((𝑛 ≠ 1𝑜𝑛𝐷) → ∃𝑚𝑝𝜂)
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 ((𝑛 ≠ 1𝑜𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
Distinct variable groups:   𝐴,𝑓,   𝐴,𝑚,𝑓   𝐴,𝑝,𝑓   ,𝐺,𝑖,𝑦   𝑅,𝑓,   𝑅,𝑚   𝑅,𝑝   𝜂,𝑓   𝑓,𝑖,𝑦   𝑓,𝑛,   𝑥,𝑓,   𝜑,   𝜓,   𝑚,𝑛   𝜑,𝑚   𝜓,𝑚   𝑥,𝑚   𝑛,𝑝   𝜑,𝑝   𝜓,𝑝   𝜃,𝑝   𝑥,𝑝
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓,𝑖,𝑛)   𝜓(𝑥,𝑦,𝑓,𝑖,𝑛)   𝜒(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜃(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛)   𝜏(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜂(𝑥,𝑦,,𝑖,𝑚,𝑛,𝑝)   𝐴(𝑥,𝑦,𝑖,𝑛)   𝐷(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝑅(𝑥,𝑦,𝑖,𝑛)   𝐺(𝑥,𝑓,𝑚,𝑛,𝑝)   𝜑′(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜓′(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜒′(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜑″(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜓″(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜑0(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜓0(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜑1(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)   𝜓1(𝑥,𝑦,𝑓,,𝑖,𝑚,𝑛,𝑝)

Proof of Theorem bnj607
StepHypRef Expression
1 bnj607.37 . . . . 5 ((𝑛 ≠ 1𝑜𝑛𝐷) → ∃𝑚𝑝𝜂)
21anim1i 590 . . . 4 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → (∃𝑚𝑝𝜂𝜃))
3 nfv 1830 . . . . . . 7 𝑝𝜃
4319.41 2090 . . . . . 6 (∃𝑝(𝜂𝜃) ↔ (∃𝑝𝜂𝜃))
54exbii 1764 . . . . 5 (∃𝑚𝑝(𝜂𝜃) ↔ ∃𝑚(∃𝑝𝜂𝜃))
6 bnj607.5 . . . . . . . 8 (𝜃 ↔ ∀𝑚𝐷 (𝑚 E 𝑛[𝑚 / 𝑛]𝜒))
76bnj1095 30106 . . . . . . 7 (𝜃 → ∀𝑚𝜃)
87nf5i 2011 . . . . . 6 𝑚𝜃
9819.41 2090 . . . . 5 (∃𝑚(∃𝑝𝜂𝜃) ↔ (∃𝑚𝑝𝜂𝜃))
105, 9bitr2i 264 . . . 4 ((∃𝑚𝑝𝜂𝜃) ↔ ∃𝑚𝑝(𝜂𝜃))
112, 10sylib 207 . . 3 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → ∃𝑚𝑝(𝜂𝜃))
12 bnj607.19 . . . . . . . . . 10 (𝜂 ↔ (𝑚𝐷𝑛 = suc 𝑚𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))
1312bnj1232 30128 . . . . . . . . 9 (𝜂𝑚𝐷)
14 bnj219 30055 . . . . . . . . . 10 (𝑛 = suc 𝑚𝑚 E 𝑛)
1512, 14bnj770 30087 . . . . . . . . 9 (𝜂𝑚 E 𝑛)
1613, 15jca 553 . . . . . . . 8 (𝜂 → (𝑚𝐷𝑚 E 𝑛))
1716anim1i 590 . . . . . . 7 ((𝜂𝜃) → ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
18 bnj170 30017 . . . . . . 7 ((𝜃𝑚𝐷𝑚 E 𝑛) ↔ ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
1917, 18sylibr 223 . . . . . 6 ((𝜂𝜃) → (𝜃𝑚𝐷𝑚 E 𝑛))
20 bnj607.38 . . . . . 6 ((𝜃𝑚𝐷𝑚 E 𝑛) → 𝜒′)
2119, 20syl 17 . . . . 5 ((𝜂𝜃) → 𝜒′)
22 simpl 472 . . . . 5 ((𝜂𝜃) → 𝜂)
2321, 22jca 553 . . . 4 ((𝜂𝜃) → (𝜒′𝜂))
24232eximi 1753 . . 3 (∃𝑚𝑝(𝜂𝜃) → ∃𝑚𝑝(𝜒′𝜂))
25 bnj607.31 . . . . . . . . . . . 12 (𝜒′ ↔ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
2625biimpi 205 . . . . . . . . . . 11 (𝜒′ → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
27 euex 2482 . . . . . . . . . . 11 (∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
2826, 27syl6 34 . . . . . . . . . 10 (𝜒′ → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
2928impcom 445 . . . . . . . . 9 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
30 bnj607.17 . . . . . . . . 9 (𝜏 ↔ (𝑓 Fn 𝑚𝜑′𝜓′))
3129, 30bnj1198 30120 . . . . . . . 8 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓𝜏)
3231adantrr 749 . . . . . . 7 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ (𝜒′𝜂)) → ∃𝑓𝜏)
33 id 22 . . . . . . . . . . 11 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝑅 FrSe 𝐴𝜏𝜂))
34333com23 1263 . . . . . . . . . 10 ((𝑅 FrSe 𝐴𝜂𝜏) → (𝑅 FrSe 𝐴𝜏𝜂))
35343expia 1259 . . . . . . . . 9 ((𝑅 FrSe 𝐴𝜂) → (𝜏 → (𝑅 FrSe 𝐴𝜏𝜂)))
3635eximdv 1833 . . . . . . . 8 ((𝑅 FrSe 𝐴𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑅 FrSe 𝐴𝜏𝜂)))
3736ad2ant2rl 781 . . . . . . 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 1235 . . . . . . 7 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝐺 Fn 𝑛𝜑″𝜓″))
4342eximi 1752 . . . . . 6 (∃𝑓(𝑅 FrSe 𝐴𝜏𝜂) → ∃𝑓(𝐺 Fn 𝑛𝜑″𝜓″))
44 nfe1 2014 . . . . . . 7 𝑓𝑓(𝑓 Fn 𝑛𝜑𝜓)
45 bnj607.28 . . . . . . . . 9 𝐺 ∈ V
46 nfcv 2751 . . . . . . . . . 10 𝐺
47 nfv 1830 . . . . . . . . . . 11 𝐺 Fn 𝑛
48 bnj607.300 . . . . . . . . . . . 12 (𝜑1[𝐺 / ]𝜑0)
49 nfsbc1v 3422 . . . . . . . . . . . 12 [𝐺 / ]𝜑0
5048, 49nfxfr 1771 . . . . . . . . . . 11 𝜑1
51 bnj607.301 . . . . . . . . . . . 12 (𝜓1[𝐺 / ]𝜓0)
52 nfsbc1v 3422 . . . . . . . . . . . 12 [𝐺 / ]𝜓0
5351, 52nfxfr 1771 . . . . . . . . . . 11 𝜓1
5447, 50, 53nf3an 1819 . . . . . . . . . 10 (𝐺 Fn 𝑛𝜑1𝜓1)
55 fneq1 5893 . . . . . . . . . . 11 ( = 𝐺 → ( Fn 𝑛𝐺 Fn 𝑛))
56 sbceq1a 3413 . . . . . . . . . . . 12 ( = 𝐺 → (𝜑0[𝐺 / ]𝜑0))
5756, 48syl6bbr 277 . . . . . . . . . . 11 ( = 𝐺 → (𝜑0𝜑1))
58 sbceq1a 3413 . . . . . . . . . . . 12 ( = 𝐺 → (𝜓0[𝐺 / ]𝜓0))
5958, 51syl6bbr 277 . . . . . . . . . . 11 ( = 𝐺 → (𝜓0𝜓1))
6055, 57, 593anbi123d 1391 . . . . . . . . . 10 ( = 𝐺 → (( Fn 𝑛𝜑0𝜓0) ↔ (𝐺 Fn 𝑛𝜑1𝜓1)))
6146, 54, 60spcegf 3262 . . . . . . . . 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 30202 . . . . . . . . . . . . 13 (𝜑0 ↔ (‘∅) = pred(𝑥, 𝐴, 𝑅))
6766, 48, 45bnj526 30212 . . . . . . . . . . . 12 (𝜑1 ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅))
6863, 67bitr4i 266 . . . . . . . . . . 11 (𝜑″𝜑1)
69 bnj607.33 . . . . . . . . . . . 12 (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝐺‘suc 𝑖) = 𝑦 ∈ (𝐺𝑖) pred(𝑦, 𝐴, 𝑅)))
70 bnj607.2 . . . . . . . . . . . . . 14 (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
71 bnj607.401 . . . . . . . . . . . . . 14 (𝜓0[ / 𝑓]𝜓)
72 vex 3176 . . . . . . . . . . . . . 14 ∈ V
7370, 71, 72bnj540 30216 . . . . . . . . . . . . 13 (𝜓0 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (‘suc 𝑖) = 𝑦 ∈ (𝑖) pred(𝑦, 𝐴, 𝑅)))
7473, 51, 45bnj540 30216 . . . . . . . . . . . 12 (𝜓1 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝐺‘suc 𝑖) = 𝑦 ∈ (𝐺𝑖) pred(𝑦, 𝐴, 𝑅)))
7569, 74bitr4i 266 . . . . . . . . . . 11 (𝜓″𝜓1)
7668, 75anbi12i 729 . . . . . . . . . 10 ((𝜑″𝜓″) ↔ (𝜑1𝜓1))
7776anbi2i 726 . . . . . . . . 9 ((𝐺 Fn 𝑛 ∧ (𝜑″𝜓″)) ↔ (𝐺 Fn 𝑛 ∧ (𝜑1𝜓1)))
78 3anass 1035 . . . . . . . . 9 ((𝐺 Fn 𝑛𝜑″𝜓″) ↔ (𝐺 Fn 𝑛 ∧ (𝜑″𝜓″)))
79 3anass 1035 . . . . . . . . 9 ((𝐺 Fn 𝑛𝜑1𝜓1) ↔ (𝐺 Fn 𝑛 ∧ (𝜑1𝜓1)))
8077, 78, 793bitr4i 291 . . . . . . . 8 ((𝐺 Fn 𝑛𝜑″𝜓″) ↔ (𝐺 Fn 𝑛𝜑1𝜓1))
81 nfv 1830 . . . . . . . . 9 (𝑓 Fn 𝑛𝜑𝜓)
82 nfv 1830 . . . . . . . . . 10 𝑓 Fn 𝑛
83 nfsbc1v 3422 . . . . . . . . . . 11 𝑓[ / 𝑓]𝜑
8464, 83nfxfr 1771 . . . . . . . . . 10 𝑓𝜑0
85 nfsbc1v 3422 . . . . . . . . . . 11 𝑓[ / 𝑓]𝜓
8671, 85nfxfr 1771 . . . . . . . . . 10 𝑓𝜓0
8782, 84, 86nf3an 1819 . . . . . . . . 9 𝑓( Fn 𝑛𝜑0𝜓0)
88 fneq1 5893 . . . . . . . . . 10 (𝑓 = → (𝑓 Fn 𝑛 Fn 𝑛))
89 sbceq1a 3413 . . . . . . . . . . 11 (𝑓 = → (𝜑[ / 𝑓]𝜑))
9089, 64syl6bbr 277 . . . . . . . . . 10 (𝑓 = → (𝜑𝜑0))
91 sbceq1a 3413 . . . . . . . . . . 11 (𝑓 = → (𝜓[ / 𝑓]𝜓))
9291, 71syl6bbr 277 . . . . . . . . . 10 (𝑓 = → (𝜓𝜓0))
9388, 90, 923anbi123d 1391 . . . . . . . . 9 (𝑓 = → ((𝑓 Fn 𝑛𝜑𝜓) ↔ ( Fn 𝑛𝜑0𝜓0)))
9481, 87, 93cbvex 2260 . . . . . . . 8 (∃𝑓(𝑓 Fn 𝑛𝜑𝜓) ↔ ∃( Fn 𝑛𝜑0𝜓0))
9562, 80, 943imtr4i 280 . . . . . . 7 ((𝐺 Fn 𝑛𝜑″𝜓″) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9644, 95exlimi 2073 . . . . . 6 (∃𝑓(𝐺 Fn 𝑛𝜑″𝜓″) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9738, 43, 963syl 18 . . . . 5 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ (𝜒′𝜂)) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9897expcom 450 . . . 4 ((𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
9998exlimivv 1847 . . 3 (∃𝑚𝑝(𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
10011, 24, 993syl 18 . 2 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
1011003impa 1251 1 ((𝑛 ≠ 1𝑜𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∃!weu 2458   ≠ wne 2780  ∀wral 2896  Vcvv 3173  [wsbc 3402  ∅c0 3874  ∪ ciun 4455   class class class wbr 4583   E cep 4947  suc csuc 5642   Fn wfn 5799  ‘cfv 5804  ωcom 6957  1𝑜c1o 7440   ∧ w-bnj17 30005   predc-bnj14 30007   FrSe w-bnj15 30011 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-eprel 4949  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812  df-bnj17 30006 This theorem is referenced by:  bnj600  30243
 Copyright terms: Public domain W3C validator