MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vdwlem1 Structured version   Visualization version   GIF version

Theorem vdwlem1 16916
Description: Lemma for vdw 16929. (Contributed by Mario Carneiro, 12-Sep-2014.)
Hypotheses
Ref Expression
vdwlem1.r (πœ‘ β†’ 𝑅 ∈ Fin)
vdwlem1.k (πœ‘ β†’ 𝐾 ∈ β„•)
vdwlem1.w (πœ‘ β†’ π‘Š ∈ β„•)
vdwlem1.f (πœ‘ β†’ 𝐹:(1...π‘Š)βŸΆπ‘…)
vdwlem1.a (πœ‘ β†’ 𝐴 ∈ β„•)
vdwlem1.m (πœ‘ β†’ 𝑀 ∈ β„•)
vdwlem1.d (πœ‘ β†’ 𝐷:(1...𝑀)βŸΆβ„•)
vdwlem1.s (πœ‘ β†’ βˆ€π‘– ∈ (1...𝑀)((𝐴 + (π·β€˜π‘–))(APβ€˜πΎ)(π·β€˜π‘–)) βŠ† (◑𝐹 β€œ {(πΉβ€˜(𝐴 + (π·β€˜π‘–)))}))
vdwlem1.i (πœ‘ β†’ 𝐼 ∈ (1...𝑀))
vdwlem1.e (πœ‘ β†’ (πΉβ€˜π΄) = (πΉβ€˜(𝐴 + (π·β€˜πΌ))))
Assertion
Ref Expression
vdwlem1 (πœ‘ β†’ (𝐾 + 1) MonoAP 𝐹)
Distinct variable groups:   𝐴,𝑖   𝐷,𝑖   𝑖,𝐼   𝑖,𝐾   𝑖,𝐹   𝑖,𝑀   πœ‘,𝑖   𝑅,𝑖   𝑖,π‘Š

Proof of Theorem vdwlem1
Dummy variables π‘Ž 𝑐 𝑑 π‘š are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vdwlem1.a . . . 4 (πœ‘ β†’ 𝐴 ∈ β„•)
2 vdwlem1.d . . . . 5 (πœ‘ β†’ 𝐷:(1...𝑀)βŸΆβ„•)
3 vdwlem1.i . . . . 5 (πœ‘ β†’ 𝐼 ∈ (1...𝑀))
42, 3ffvelcdmd 7087 . . . 4 (πœ‘ β†’ (π·β€˜πΌ) ∈ β„•)
5 vdwlem1.k . . . . . . 7 (πœ‘ β†’ 𝐾 ∈ β„•)
65nnnn0d 12534 . . . . . 6 (πœ‘ β†’ 𝐾 ∈ β„•0)
7 vdwapun 16909 . . . . . 6 ((𝐾 ∈ β„•0 ∧ 𝐴 ∈ β„• ∧ (π·β€˜πΌ) ∈ β„•) β†’ (𝐴(APβ€˜(𝐾 + 1))(π·β€˜πΌ)) = ({𝐴} βˆͺ ((𝐴 + (π·β€˜πΌ))(APβ€˜πΎ)(π·β€˜πΌ))))
86, 1, 4, 7syl3anc 1371 . . . . 5 (πœ‘ β†’ (𝐴(APβ€˜(𝐾 + 1))(π·β€˜πΌ)) = ({𝐴} βˆͺ ((𝐴 + (π·β€˜πΌ))(APβ€˜πΎ)(π·β€˜πΌ))))
91nnred 12229 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ ℝ)
10 vdwlem1.m . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑀 ∈ β„•)
11 nnuz 12867 . . . . . . . . . . . . . . 15 β„• = (β„€β‰₯β€˜1)
1210, 11eleqtrdi 2843 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑀 ∈ (β„€β‰₯β€˜1))
13 eluzfz1 13510 . . . . . . . . . . . . . 14 (𝑀 ∈ (β„€β‰₯β€˜1) β†’ 1 ∈ (1...𝑀))
1412, 13syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 1 ∈ (1...𝑀))
152, 14ffvelcdmd 7087 . . . . . . . . . . . 12 (πœ‘ β†’ (π·β€˜1) ∈ β„•)
161, 15nnaddcld 12266 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 + (π·β€˜1)) ∈ β„•)
1716nnred 12229 . . . . . . . . . 10 (πœ‘ β†’ (𝐴 + (π·β€˜1)) ∈ ℝ)
18 vdwlem1.w . . . . . . . . . . 11 (πœ‘ β†’ π‘Š ∈ β„•)
1918nnred 12229 . . . . . . . . . 10 (πœ‘ β†’ π‘Š ∈ ℝ)
2015nnrpd 13016 . . . . . . . . . . . 12 (πœ‘ β†’ (π·β€˜1) ∈ ℝ+)
219, 20ltaddrpd 13051 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 < (𝐴 + (π·β€˜1)))
229, 17, 21ltled 11364 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ≀ (𝐴 + (π·β€˜1)))
23 fveq2 6891 . . . . . . . . . . . . . 14 (𝑖 = 1 β†’ (π·β€˜π‘–) = (π·β€˜1))
2423oveq2d 7427 . . . . . . . . . . . . 13 (𝑖 = 1 β†’ (𝐴 + (π·β€˜π‘–)) = (𝐴 + (π·β€˜1)))
2524eleq1d 2818 . . . . . . . . . . . 12 (𝑖 = 1 β†’ ((𝐴 + (π·β€˜π‘–)) ∈ (1...π‘Š) ↔ (𝐴 + (π·β€˜1)) ∈ (1...π‘Š)))
26 vdwlem1.s . . . . . . . . . . . . . . . 16 (πœ‘ β†’ βˆ€π‘– ∈ (1...𝑀)((𝐴 + (π·β€˜π‘–))(APβ€˜πΎ)(π·β€˜π‘–)) βŠ† (◑𝐹 β€œ {(πΉβ€˜(𝐴 + (π·β€˜π‘–)))}))
2726r19.21bi 3248 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ ((𝐴 + (π·β€˜π‘–))(APβ€˜πΎ)(π·β€˜π‘–)) βŠ† (◑𝐹 β€œ {(πΉβ€˜(𝐴 + (π·β€˜π‘–)))}))
28 cnvimass 6080 . . . . . . . . . . . . . . . . 17 (◑𝐹 β€œ {(πΉβ€˜(𝐴 + (π·β€˜π‘–)))}) βŠ† dom 𝐹
29 vdwlem1.f . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐹:(1...π‘Š)βŸΆπ‘…)
3028, 29fssdm 6737 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (◑𝐹 β€œ {(πΉβ€˜(𝐴 + (π·β€˜π‘–)))}) βŠ† (1...π‘Š))
3130adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ (◑𝐹 β€œ {(πΉβ€˜(𝐴 + (π·β€˜π‘–)))}) βŠ† (1...π‘Š))
3227, 31sstrd 3992 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ ((𝐴 + (π·β€˜π‘–))(APβ€˜πΎ)(π·β€˜π‘–)) βŠ† (1...π‘Š))
33 nnm1nn0 12515 . . . . . . . . . . . . . . . . . . . 20 (𝐾 ∈ β„• β†’ (𝐾 βˆ’ 1) ∈ β„•0)
345, 33syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝐾 βˆ’ 1) ∈ β„•0)
35 nn0uz 12866 . . . . . . . . . . . . . . . . . . 19 β„•0 = (β„€β‰₯β€˜0)
3634, 35eleqtrdi 2843 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐾 βˆ’ 1) ∈ (β„€β‰₯β€˜0))
37 eluzfz1 13510 . . . . . . . . . . . . . . . . . 18 ((𝐾 βˆ’ 1) ∈ (β„€β‰₯β€˜0) β†’ 0 ∈ (0...(𝐾 βˆ’ 1)))
3836, 37syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 0 ∈ (0...(𝐾 βˆ’ 1)))
3938adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ 0 ∈ (0...(𝐾 βˆ’ 1)))
402ffvelcdmda 7086 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ (π·β€˜π‘–) ∈ β„•)
4140nncnd 12230 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ (π·β€˜π‘–) ∈ β„‚)
4241mul02d 11414 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ (0 Β· (π·β€˜π‘–)) = 0)
4342oveq2d 7427 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ ((𝐴 + (π·β€˜π‘–)) + (0 Β· (π·β€˜π‘–))) = ((𝐴 + (π·β€˜π‘–)) + 0))
441adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ 𝐴 ∈ β„•)
4544, 40nnaddcld 12266 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ (𝐴 + (π·β€˜π‘–)) ∈ β„•)
4645nncnd 12230 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ (𝐴 + (π·β€˜π‘–)) ∈ β„‚)
4746addridd 11416 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ ((𝐴 + (π·β€˜π‘–)) + 0) = (𝐴 + (π·β€˜π‘–)))
4843, 47eqtr2d 2773 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ (𝐴 + (π·β€˜π‘–)) = ((𝐴 + (π·β€˜π‘–)) + (0 Β· (π·β€˜π‘–))))
49 oveq1 7418 . . . . . . . . . . . . . . . . . 18 (π‘š = 0 β†’ (π‘š Β· (π·β€˜π‘–)) = (0 Β· (π·β€˜π‘–)))
5049oveq2d 7427 . . . . . . . . . . . . . . . . 17 (π‘š = 0 β†’ ((𝐴 + (π·β€˜π‘–)) + (π‘š Β· (π·β€˜π‘–))) = ((𝐴 + (π·β€˜π‘–)) + (0 Β· (π·β€˜π‘–))))
5150rspceeqv 3633 . . . . . . . . . . . . . . . 16 ((0 ∈ (0...(𝐾 βˆ’ 1)) ∧ (𝐴 + (π·β€˜π‘–)) = ((𝐴 + (π·β€˜π‘–)) + (0 Β· (π·β€˜π‘–)))) β†’ βˆƒπ‘š ∈ (0...(𝐾 βˆ’ 1))(𝐴 + (π·β€˜π‘–)) = ((𝐴 + (π·β€˜π‘–)) + (π‘š Β· (π·β€˜π‘–))))
5239, 48, 51syl2anc 584 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ βˆƒπ‘š ∈ (0...(𝐾 βˆ’ 1))(𝐴 + (π·β€˜π‘–)) = ((𝐴 + (π·β€˜π‘–)) + (π‘š Β· (π·β€˜π‘–))))
535adantr 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ 𝐾 ∈ β„•)
5453nnnn0d 12534 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ 𝐾 ∈ β„•0)
55 vdwapval 16908 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ β„•0 ∧ (𝐴 + (π·β€˜π‘–)) ∈ β„• ∧ (π·β€˜π‘–) ∈ β„•) β†’ ((𝐴 + (π·β€˜π‘–)) ∈ ((𝐴 + (π·β€˜π‘–))(APβ€˜πΎ)(π·β€˜π‘–)) ↔ βˆƒπ‘š ∈ (0...(𝐾 βˆ’ 1))(𝐴 + (π·β€˜π‘–)) = ((𝐴 + (π·β€˜π‘–)) + (π‘š Β· (π·β€˜π‘–)))))
5654, 45, 40, 55syl3anc 1371 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ ((𝐴 + (π·β€˜π‘–)) ∈ ((𝐴 + (π·β€˜π‘–))(APβ€˜πΎ)(π·β€˜π‘–)) ↔ βˆƒπ‘š ∈ (0...(𝐾 βˆ’ 1))(𝐴 + (π·β€˜π‘–)) = ((𝐴 + (π·β€˜π‘–)) + (π‘š Β· (π·β€˜π‘–)))))
5752, 56mpbird 256 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ (𝐴 + (π·β€˜π‘–)) ∈ ((𝐴 + (π·β€˜π‘–))(APβ€˜πΎ)(π·β€˜π‘–)))
5832, 57sseldd 3983 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) β†’ (𝐴 + (π·β€˜π‘–)) ∈ (1...π‘Š))
5958ralrimiva 3146 . . . . . . . . . . . 12 (πœ‘ β†’ βˆ€π‘– ∈ (1...𝑀)(𝐴 + (π·β€˜π‘–)) ∈ (1...π‘Š))
6025, 59, 14rspcdva 3613 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 + (π·β€˜1)) ∈ (1...π‘Š))
61 elfzle2 13507 . . . . . . . . . . 11 ((𝐴 + (π·β€˜1)) ∈ (1...π‘Š) β†’ (𝐴 + (π·β€˜1)) ≀ π‘Š)
6260, 61syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝐴 + (π·β€˜1)) ≀ π‘Š)
639, 17, 19, 22, 62letrd 11373 . . . . . . . . 9 (πœ‘ β†’ 𝐴 ≀ π‘Š)
641, 11eleqtrdi 2843 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ (β„€β‰₯β€˜1))
6518nnzd 12587 . . . . . . . . . 10 (πœ‘ β†’ π‘Š ∈ β„€)
66 elfz5 13495 . . . . . . . . . 10 ((𝐴 ∈ (β„€β‰₯β€˜1) ∧ π‘Š ∈ β„€) β†’ (𝐴 ∈ (1...π‘Š) ↔ 𝐴 ≀ π‘Š))
6764, 65, 66syl2anc 584 . . . . . . . . 9 (πœ‘ β†’ (𝐴 ∈ (1...π‘Š) ↔ 𝐴 ≀ π‘Š))
6863, 67mpbird 256 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ (1...π‘Š))
69 eqidd 2733 . . . . . . . 8 (πœ‘ β†’ (πΉβ€˜π΄) = (πΉβ€˜π΄))
70 ffn 6717 . . . . . . . . 9 (𝐹:(1...π‘Š)βŸΆπ‘… β†’ 𝐹 Fn (1...π‘Š))
71 fniniseg 7061 . . . . . . . . 9 (𝐹 Fn (1...π‘Š) β†’ (𝐴 ∈ (◑𝐹 β€œ {(πΉβ€˜π΄)}) ↔ (𝐴 ∈ (1...π‘Š) ∧ (πΉβ€˜π΄) = (πΉβ€˜π΄))))
7229, 70, 713syl 18 . . . . . . . 8 (πœ‘ β†’ (𝐴 ∈ (◑𝐹 β€œ {(πΉβ€˜π΄)}) ↔ (𝐴 ∈ (1...π‘Š) ∧ (πΉβ€˜π΄) = (πΉβ€˜π΄))))
7368, 69, 72mpbir2and 711 . . . . . . 7 (πœ‘ β†’ 𝐴 ∈ (◑𝐹 β€œ {(πΉβ€˜π΄)}))
7473snssd 4812 . . . . . 6 (πœ‘ β†’ {𝐴} βŠ† (◑𝐹 β€œ {(πΉβ€˜π΄)}))
75 fveq2 6891 . . . . . . . . . . 11 (𝑖 = 𝐼 β†’ (π·β€˜π‘–) = (π·β€˜πΌ))
7675oveq2d 7427 . . . . . . . . . 10 (𝑖 = 𝐼 β†’ (𝐴 + (π·β€˜π‘–)) = (𝐴 + (π·β€˜πΌ)))
7776, 75oveq12d 7429 . . . . . . . . 9 (𝑖 = 𝐼 β†’ ((𝐴 + (π·β€˜π‘–))(APβ€˜πΎ)(π·β€˜π‘–)) = ((𝐴 + (π·β€˜πΌ))(APβ€˜πΎ)(π·β€˜πΌ)))
7876fveq2d 6895 . . . . . . . . . . 11 (𝑖 = 𝐼 β†’ (πΉβ€˜(𝐴 + (π·β€˜π‘–))) = (πΉβ€˜(𝐴 + (π·β€˜πΌ))))
7978sneqd 4640 . . . . . . . . . 10 (𝑖 = 𝐼 β†’ {(πΉβ€˜(𝐴 + (π·β€˜π‘–)))} = {(πΉβ€˜(𝐴 + (π·β€˜πΌ)))})
8079imaeq2d 6059 . . . . . . . . 9 (𝑖 = 𝐼 β†’ (◑𝐹 β€œ {(πΉβ€˜(𝐴 + (π·β€˜π‘–)))}) = (◑𝐹 β€œ {(πΉβ€˜(𝐴 + (π·β€˜πΌ)))}))
8177, 80sseq12d 4015 . . . . . . . 8 (𝑖 = 𝐼 β†’ (((𝐴 + (π·β€˜π‘–))(APβ€˜πΎ)(π·β€˜π‘–)) βŠ† (◑𝐹 β€œ {(πΉβ€˜(𝐴 + (π·β€˜π‘–)))}) ↔ ((𝐴 + (π·β€˜πΌ))(APβ€˜πΎ)(π·β€˜πΌ)) βŠ† (◑𝐹 β€œ {(πΉβ€˜(𝐴 + (π·β€˜πΌ)))})))
8281, 26, 3rspcdva 3613 . . . . . . 7 (πœ‘ β†’ ((𝐴 + (π·β€˜πΌ))(APβ€˜πΎ)(π·β€˜πΌ)) βŠ† (◑𝐹 β€œ {(πΉβ€˜(𝐴 + (π·β€˜πΌ)))}))
83 vdwlem1.e . . . . . . . . 9 (πœ‘ β†’ (πΉβ€˜π΄) = (πΉβ€˜(𝐴 + (π·β€˜πΌ))))
8483sneqd 4640 . . . . . . . 8 (πœ‘ β†’ {(πΉβ€˜π΄)} = {(πΉβ€˜(𝐴 + (π·β€˜πΌ)))})
8584imaeq2d 6059 . . . . . . 7 (πœ‘ β†’ (◑𝐹 β€œ {(πΉβ€˜π΄)}) = (◑𝐹 β€œ {(πΉβ€˜(𝐴 + (π·β€˜πΌ)))}))
8682, 85sseqtrrd 4023 . . . . . 6 (πœ‘ β†’ ((𝐴 + (π·β€˜πΌ))(APβ€˜πΎ)(π·β€˜πΌ)) βŠ† (◑𝐹 β€œ {(πΉβ€˜π΄)}))
8774, 86unssd 4186 . . . . 5 (πœ‘ β†’ ({𝐴} βˆͺ ((𝐴 + (π·β€˜πΌ))(APβ€˜πΎ)(π·β€˜πΌ))) βŠ† (◑𝐹 β€œ {(πΉβ€˜π΄)}))
888, 87eqsstrd 4020 . . . 4 (πœ‘ β†’ (𝐴(APβ€˜(𝐾 + 1))(π·β€˜πΌ)) βŠ† (◑𝐹 β€œ {(πΉβ€˜π΄)}))
89 oveq1 7418 . . . . . 6 (π‘Ž = 𝐴 β†’ (π‘Ž(APβ€˜(𝐾 + 1))𝑑) = (𝐴(APβ€˜(𝐾 + 1))𝑑))
9089sseq1d 4013 . . . . 5 (π‘Ž = 𝐴 β†’ ((π‘Ž(APβ€˜(𝐾 + 1))𝑑) βŠ† (◑𝐹 β€œ {(πΉβ€˜π΄)}) ↔ (𝐴(APβ€˜(𝐾 + 1))𝑑) βŠ† (◑𝐹 β€œ {(πΉβ€˜π΄)})))
91 oveq2 7419 . . . . . 6 (𝑑 = (π·β€˜πΌ) β†’ (𝐴(APβ€˜(𝐾 + 1))𝑑) = (𝐴(APβ€˜(𝐾 + 1))(π·β€˜πΌ)))
9291sseq1d 4013 . . . . 5 (𝑑 = (π·β€˜πΌ) β†’ ((𝐴(APβ€˜(𝐾 + 1))𝑑) βŠ† (◑𝐹 β€œ {(πΉβ€˜π΄)}) ↔ (𝐴(APβ€˜(𝐾 + 1))(π·β€˜πΌ)) βŠ† (◑𝐹 β€œ {(πΉβ€˜π΄)})))
9390, 92rspc2ev 3624 . . . 4 ((𝐴 ∈ β„• ∧ (π·β€˜πΌ) ∈ β„• ∧ (𝐴(APβ€˜(𝐾 + 1))(π·β€˜πΌ)) βŠ† (◑𝐹 β€œ {(πΉβ€˜π΄)})) β†’ βˆƒπ‘Ž ∈ β„• βˆƒπ‘‘ ∈ β„• (π‘Ž(APβ€˜(𝐾 + 1))𝑑) βŠ† (◑𝐹 β€œ {(πΉβ€˜π΄)}))
941, 4, 88, 93syl3anc 1371 . . 3 (πœ‘ β†’ βˆƒπ‘Ž ∈ β„• βˆƒπ‘‘ ∈ β„• (π‘Ž(APβ€˜(𝐾 + 1))𝑑) βŠ† (◑𝐹 β€œ {(πΉβ€˜π΄)}))
95 fvex 6904 . . . 4 (πΉβ€˜π΄) ∈ V
96 sneq 4638 . . . . . . 7 (𝑐 = (πΉβ€˜π΄) β†’ {𝑐} = {(πΉβ€˜π΄)})
9796imaeq2d 6059 . . . . . 6 (𝑐 = (πΉβ€˜π΄) β†’ (◑𝐹 β€œ {𝑐}) = (◑𝐹 β€œ {(πΉβ€˜π΄)}))
9897sseq2d 4014 . . . . 5 (𝑐 = (πΉβ€˜π΄) β†’ ((π‘Ž(APβ€˜(𝐾 + 1))𝑑) βŠ† (◑𝐹 β€œ {𝑐}) ↔ (π‘Ž(APβ€˜(𝐾 + 1))𝑑) βŠ† (◑𝐹 β€œ {(πΉβ€˜π΄)})))
99982rexbidv 3219 . . . 4 (𝑐 = (πΉβ€˜π΄) β†’ (βˆƒπ‘Ž ∈ β„• βˆƒπ‘‘ ∈ β„• (π‘Ž(APβ€˜(𝐾 + 1))𝑑) βŠ† (◑𝐹 β€œ {𝑐}) ↔ βˆƒπ‘Ž ∈ β„• βˆƒπ‘‘ ∈ β„• (π‘Ž(APβ€˜(𝐾 + 1))𝑑) βŠ† (◑𝐹 β€œ {(πΉβ€˜π΄)})))
10095, 99spcev 3596 . . 3 (βˆƒπ‘Ž ∈ β„• βˆƒπ‘‘ ∈ β„• (π‘Ž(APβ€˜(𝐾 + 1))𝑑) βŠ† (◑𝐹 β€œ {(πΉβ€˜π΄)}) β†’ βˆƒπ‘βˆƒπ‘Ž ∈ β„• βˆƒπ‘‘ ∈ β„• (π‘Ž(APβ€˜(𝐾 + 1))𝑑) βŠ† (◑𝐹 β€œ {𝑐}))
10194, 100syl 17 . 2 (πœ‘ β†’ βˆƒπ‘βˆƒπ‘Ž ∈ β„• βˆƒπ‘‘ ∈ β„• (π‘Ž(APβ€˜(𝐾 + 1))𝑑) βŠ† (◑𝐹 β€œ {𝑐}))
102 ovex 7444 . . 3 (1...π‘Š) ∈ V
103 peano2nn0 12514 . . . 4 (𝐾 ∈ β„•0 β†’ (𝐾 + 1) ∈ β„•0)
1046, 103syl 17 . . 3 (πœ‘ β†’ (𝐾 + 1) ∈ β„•0)
105102, 104, 29vdwmc 16913 . 2 (πœ‘ β†’ ((𝐾 + 1) MonoAP 𝐹 ↔ βˆƒπ‘βˆƒπ‘Ž ∈ β„• βˆƒπ‘‘ ∈ β„• (π‘Ž(APβ€˜(𝐾 + 1))𝑑) βŠ† (◑𝐹 β€œ {𝑐})))
106101, 105mpbird 256 1 (πœ‘ β†’ (𝐾 + 1) MonoAP 𝐹)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  βˆ€wral 3061  βˆƒwrex 3070   βˆͺ cun 3946   βŠ† wss 3948  {csn 4628   class class class wbr 5148  β—‘ccnv 5675   β€œ cima 5679   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411  Fincfn 8941  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117   ≀ cle 11251   βˆ’ cmin 11446  β„•cn 12214  β„•0cn0 12474  β„€cz 12560  β„€β‰₯cuz 12824  ...cfz 13486  APcvdwa 16900   MonoAP cvdwm 16901
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-nn 12215  df-n0 12475  df-z 12561  df-uz 12825  df-rp 12977  df-fz 13487  df-vdwap 16903  df-vdwmc 16904
This theorem is referenced by:  vdwlem6  16921
  Copyright terms: Public domain W3C validator