Users' Mathboxes 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 30971
Description: Technical lemma for bnj852 30976. 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 592 . . . 4 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → (∃𝑚𝑝𝜂𝜃))
3 nfv 1842 . . . . . . 7 𝑝𝜃
4319.41 2102 . . . . . 6 (∃𝑝(𝜂𝜃) ↔ (∃𝑝𝜂𝜃))
54exbii 1773 . . . . 5 (∃𝑚𝑝(𝜂𝜃) ↔ ∃𝑚(∃𝑝𝜂𝜃))
6 bnj607.5 . . . . . . . 8 (𝜃 ↔ ∀𝑚𝐷 (𝑚 E 𝑛[𝑚 / 𝑛]𝜒))
76bnj1095 30837 . . . . . . 7 (𝜃 → ∀𝑚𝜃)
87nf5i 2023 . . . . . 6 𝑚𝜃
9819.41 2102 . . . . 5 (∃𝑚(∃𝑝𝜂𝜃) ↔ (∃𝑚𝑝𝜂𝜃))
105, 9bitr2i 265 . . . 4 ((∃𝑚𝑝𝜂𝜃) ↔ ∃𝑚𝑝(𝜂𝜃))
112, 10sylib 208 . . 3 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → ∃𝑚𝑝(𝜂𝜃))
12 bnj607.19 . . . . . . . . . 10 (𝜂 ↔ (𝑚𝐷𝑛 = suc 𝑚𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))
1312bnj1232 30859 . . . . . . . . 9 (𝜂𝑚𝐷)
14 bnj219 30786 . . . . . . . . . 10 (𝑛 = suc 𝑚𝑚 E 𝑛)
1512, 14bnj770 30818 . . . . . . . . 9 (𝜂𝑚 E 𝑛)
1613, 15jca 554 . . . . . . . 8 (𝜂 → (𝑚𝐷𝑚 E 𝑛))
1716anim1i 592 . . . . . . 7 ((𝜂𝜃) → ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
18 bnj170 30749 . . . . . . 7 ((𝜃𝑚𝐷𝑚 E 𝑛) ↔ ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
1917, 18sylibr 224 . . . . . 6 ((𝜂𝜃) → (𝜃𝑚𝐷𝑚 E 𝑛))
20 bnj607.38 . . . . . 6 ((𝜃𝑚𝐷𝑚 E 𝑛) → 𝜒′)
2119, 20syl 17 . . . . 5 ((𝜂𝜃) → 𝜒′)
22 simpl 473 . . . . 5 ((𝜂𝜃) → 𝜂)
2321, 22jca 554 . . . 4 ((𝜂𝜃) → (𝜒′𝜂))
24232eximi 1762 . . 3 (∃𝑚𝑝(𝜂𝜃) → ∃𝑚𝑝(𝜒′𝜂))
25 bnj607.31 . . . . . . . . . . . 12 (𝜒′ ↔ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
2625biimpi 206 . . . . . . . . . . 11 (𝜒′ → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
27 euex 2493 . . . . . . . . . . 11 (∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
2826, 27syl6 35 . . . . . . . . . 10 (𝜒′ → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
2928impcom 446 . . . . . . . . 9 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
30 bnj607.17 . . . . . . . . 9 (𝜏 ↔ (𝑓 Fn 𝑚𝜑′𝜓′))
3129, 30bnj1198 30851 . . . . . . . 8 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓𝜏)
3231adantrr 753 . . . . . . 7 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ (𝜒′𝜂)) → ∃𝑓𝜏)
33 id 22 . . . . . . . . . . 11 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝑅 FrSe 𝐴𝜏𝜂))
34333com23 1270 . . . . . . . . . 10 ((𝑅 FrSe 𝐴𝜂𝜏) → (𝑅 FrSe 𝐴𝜏𝜂))
35343expia 1266 . . . . . . . . 9 ((𝑅 FrSe 𝐴𝜂) → (𝜏 → (𝑅 FrSe 𝐴𝜏𝜂)))
3635eximdv 1845 . . . . . . . 8 ((𝑅 FrSe 𝐴𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑅 FrSe 𝐴𝜏𝜂)))
3736ad2ant2rl 785 . . . . . . 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 1241 . . . . . . 7 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝐺 Fn 𝑛𝜑″𝜓″))
4342eximi 1761 . . . . . 6 (∃𝑓(𝑅 FrSe 𝐴𝜏𝜂) → ∃𝑓(𝐺 Fn 𝑛𝜑″𝜓″))
44 nfe1 2026 . . . . . . 7 𝑓𝑓(𝑓 Fn 𝑛𝜑𝜓)
45 bnj607.28 . . . . . . . . 9 𝐺 ∈ V
46 nfcv 2763 . . . . . . . . . 10 𝐺
47 nfv 1842 . . . . . . . . . . 11 𝐺 Fn 𝑛
48 bnj607.300 . . . . . . . . . . . 12 (𝜑1[𝐺 / ]𝜑0)
49 nfsbc1v 3453 . . . . . . . . . . . 12 [𝐺 / ]𝜑0
5048, 49nfxfr 1778 . . . . . . . . . . 11 𝜑1
51 bnj607.301 . . . . . . . . . . . 12 (𝜓1[𝐺 / ]𝜓0)
52 nfsbc1v 3453 . . . . . . . . . . . 12 [𝐺 / ]𝜓0
5351, 52nfxfr 1778 . . . . . . . . . . 11 𝜓1
5447, 50, 53nf3an 1830 . . . . . . . . . 10 (𝐺 Fn 𝑛𝜑1𝜓1)
55 fneq1 5977 . . . . . . . . . . 11 ( = 𝐺 → ( Fn 𝑛𝐺 Fn 𝑛))
56 sbceq1a 3444 . . . . . . . . . . . 12 ( = 𝐺 → (𝜑0[𝐺 / ]𝜑0))
5756, 48syl6bbr 278 . . . . . . . . . . 11 ( = 𝐺 → (𝜑0𝜑1))
58 sbceq1a 3444 . . . . . . . . . . . 12 ( = 𝐺 → (𝜓0[𝐺 / ]𝜓0))
5958, 51syl6bbr 278 . . . . . . . . . . 11 ( = 𝐺 → (𝜓0𝜓1))
6055, 57, 593anbi123d 1398 . . . . . . . . . 10 ( = 𝐺 → (( Fn 𝑛𝜑0𝜓0) ↔ (𝐺 Fn 𝑛𝜑1𝜓1)))
6146, 54, 60spcegf 3287 . . . . . . . . 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 30933 . . . . . . . . . . . . 13 (𝜑0 ↔ (‘∅) = pred(𝑥, 𝐴, 𝑅))
6766, 48, 45bnj526 30943 . . . . . . . . . . . 12 (𝜑1 ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅))
6863, 67bitr4i 267 . . . . . . . . . . 11 (𝜑″𝜑1)
69 bnj607.33 . . . . . . . . . . . 12 (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝐺‘suc 𝑖) = 𝑦 ∈ (𝐺𝑖) pred(𝑦, 𝐴, 𝑅)))
70 bnj607.2 . . . . . . . . . . . . . 14 (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
71 bnj607.401 . . . . . . . . . . . . . 14 (𝜓0[ / 𝑓]𝜓)
72 vex 3201 . . . . . . . . . . . . . 14 ∈ V
7370, 71, 72bnj540 30947 . . . . . . . . . . . . 13 (𝜓0 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (‘suc 𝑖) = 𝑦 ∈ (𝑖) pred(𝑦, 𝐴, 𝑅)))
7473, 51, 45bnj540 30947 . . . . . . . . . . . 12 (𝜓1 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝐺‘suc 𝑖) = 𝑦 ∈ (𝐺𝑖) pred(𝑦, 𝐴, 𝑅)))
7569, 74bitr4i 267 . . . . . . . . . . 11 (𝜓″𝜓1)
7668, 75anbi12i 733 . . . . . . . . . 10 ((𝜑″𝜓″) ↔ (𝜑1𝜓1))
7776anbi2i 730 . . . . . . . . 9 ((𝐺 Fn 𝑛 ∧ (𝜑″𝜓″)) ↔ (𝐺 Fn 𝑛 ∧ (𝜑1𝜓1)))
78 3anass 1041 . . . . . . . . 9 ((𝐺 Fn 𝑛𝜑″𝜓″) ↔ (𝐺 Fn 𝑛 ∧ (𝜑″𝜓″)))
79 3anass 1041 . . . . . . . . 9 ((𝐺 Fn 𝑛𝜑1𝜓1) ↔ (𝐺 Fn 𝑛 ∧ (𝜑1𝜓1)))
8077, 78, 793bitr4i 292 . . . . . . . 8 ((𝐺 Fn 𝑛𝜑″𝜓″) ↔ (𝐺 Fn 𝑛𝜑1𝜓1))
81 nfv 1842 . . . . . . . . 9 (𝑓 Fn 𝑛𝜑𝜓)
82 nfv 1842 . . . . . . . . . 10 𝑓 Fn 𝑛
83 nfsbc1v 3453 . . . . . . . . . . 11 𝑓[ / 𝑓]𝜑
8464, 83nfxfr 1778 . . . . . . . . . 10 𝑓𝜑0
85 nfsbc1v 3453 . . . . . . . . . . 11 𝑓[ / 𝑓]𝜓
8671, 85nfxfr 1778 . . . . . . . . . 10 𝑓𝜓0
8782, 84, 86nf3an 1830 . . . . . . . . 9 𝑓( Fn 𝑛𝜑0𝜓0)
88 fneq1 5977 . . . . . . . . . 10 (𝑓 = → (𝑓 Fn 𝑛 Fn 𝑛))
89 sbceq1a 3444 . . . . . . . . . . 11 (𝑓 = → (𝜑[ / 𝑓]𝜑))
9089, 64syl6bbr 278 . . . . . . . . . 10 (𝑓 = → (𝜑𝜑0))
91 sbceq1a 3444 . . . . . . . . . . 11 (𝑓 = → (𝜓[ / 𝑓]𝜓))
9291, 71syl6bbr 278 . . . . . . . . . 10 (𝑓 = → (𝜓𝜓0))
9388, 90, 923anbi123d 1398 . . . . . . . . 9 (𝑓 = → ((𝑓 Fn 𝑛𝜑𝜓) ↔ ( Fn 𝑛𝜑0𝜓0)))
9481, 87, 93cbvex 2271 . . . . . . . 8 (∃𝑓(𝑓 Fn 𝑛𝜑𝜓) ↔ ∃( Fn 𝑛𝜑0𝜓0))
9562, 80, 943imtr4i 281 . . . . . . 7 ((𝐺 Fn 𝑛𝜑″𝜓″) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9644, 95exlimi 2085 . . . . . 6 (∃𝑓(𝐺 Fn 𝑛𝜑″𝜓″) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9738, 43, 963syl 18 . . . . 5 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ (𝜒′𝜂)) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
9897expcom 451 . . . 4 ((𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
9998exlimivv 1859 . . 3 (∃𝑚𝑝(𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
10011, 24, 993syl 18 . 2 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
1011003impa 1258 1 ((𝑛 ≠ 1𝑜𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1037   = wceq 1482  wex 1703  wcel 1989  ∃!weu 2469  wne 2793  wral 2911  Vcvv 3198  [wsbc 3433  c0 3913   ciun 4518   class class class wbr 4651   E cep 5026  suc csuc 5723   Fn wfn 5881  cfv 5886  ωcom 7062  1𝑜c1o 7550  w-bnj17 30737   predc-bnj14 30739   FrSe w-bnj15 30743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pr 4904
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-sbc 3434  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-iun 4520  df-br 4652  df-opab 4711  df-eprel 5027  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-fv 5894  df-bnj17 30738
This theorem is referenced by:  bnj600  30974
  Copyright terms: Public domain W3C validator