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

Theorem axdclem2 9791
Description: Lemma for axdc 9792. Using the full Axiom of Choice, we can construct a choice function 𝑔 on 𝒫 dom 𝑥. From this, we can build a sequence 𝐹 starting at any value 𝑠 ∈ dom 𝑥 by repeatedly applying 𝑔 to the set (𝐹𝑥) (where 𝑥 is the value from the previous iteration). (Contributed by Mario Carneiro, 25-Jan-2013.)
Hypothesis
Ref Expression
axdclem2.1 𝐹 = (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧𝑦𝑥𝑧})), 𝑠) ↾ ω)
Assertion
Ref Expression
axdclem2 (∃𝑧 𝑠𝑥𝑧 → (ran 𝑥 ⊆ dom 𝑥 → ∃𝑓𝑛 ∈ ω (𝑓𝑛)𝑥(𝑓‘suc 𝑛)))
Distinct variable groups:   𝑓,𝐹,𝑛   𝑦,𝐹,𝑧,𝑛   𝑓,𝑔,𝑥,𝑛   𝑔,𝑠,𝑦,𝑛   𝑧,𝑔   𝑥,𝑦,𝑧
Allowed substitution hints:   𝐹(𝑥,𝑔,𝑠)

Proof of Theorem axdclem2
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 frfnom 7925 . . . . . . . 8 (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧𝑦𝑥𝑧})), 𝑠) ↾ ω) Fn ω
2 axdclem2.1 . . . . . . . . 9 𝐹 = (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧𝑦𝑥𝑧})), 𝑠) ↾ ω)
32fneq1i 6323 . . . . . . . 8 (𝐹 Fn ω ↔ (rec((𝑦 ∈ V ↦ (𝑔‘{𝑧𝑦𝑥𝑧})), 𝑠) ↾ ω) Fn ω)
41, 3mpbir 232 . . . . . . 7 𝐹 Fn ω
54a1i 11 . . . . . 6 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹 Fn ω)
6 fveq2 6541 . . . . . . . . . . 11 (𝑛 = ∅ → (𝐹𝑛) = (𝐹‘∅))
7 suceq 6134 . . . . . . . . . . . 12 (𝑛 = ∅ → suc 𝑛 = suc ∅)
87fveq2d 6545 . . . . . . . . . . 11 (𝑛 = ∅ → (𝐹‘suc 𝑛) = (𝐹‘suc ∅))
96, 8breq12d 4977 . . . . . . . . . 10 (𝑛 = ∅ → ((𝐹𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘∅)𝑥(𝐹‘suc ∅)))
10 fveq2 6541 . . . . . . . . . . 11 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
11 suceq 6134 . . . . . . . . . . . 12 (𝑛 = 𝑘 → suc 𝑛 = suc 𝑘)
1211fveq2d 6545 . . . . . . . . . . 11 (𝑛 = 𝑘 → (𝐹‘suc 𝑛) = (𝐹‘suc 𝑘))
1310, 12breq12d 4977 . . . . . . . . . 10 (𝑛 = 𝑘 → ((𝐹𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹𝑘)𝑥(𝐹‘suc 𝑘)))
14 fveq2 6541 . . . . . . . . . . 11 (𝑛 = suc 𝑘 → (𝐹𝑛) = (𝐹‘suc 𝑘))
15 suceq 6134 . . . . . . . . . . . 12 (𝑛 = suc 𝑘 → suc 𝑛 = suc suc 𝑘)
1615fveq2d 6545 . . . . . . . . . . 11 (𝑛 = suc 𝑘 → (𝐹‘suc 𝑛) = (𝐹‘suc suc 𝑘))
1714, 16breq12d 4977 . . . . . . . . . 10 (𝑛 = suc 𝑘 → ((𝐹𝑛)𝑥(𝐹‘suc 𝑛) ↔ (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))
182fveq1i 6542 . . . . . . . . . . . . . . . 16 (𝐹‘∅) = ((rec((𝑦 ∈ V ↦ (𝑔‘{𝑧𝑦𝑥𝑧})), 𝑠) ↾ ω)‘∅)
19 fr0g 7926 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ V → ((rec((𝑦 ∈ V ↦ (𝑔‘{𝑧𝑦𝑥𝑧})), 𝑠) ↾ ω)‘∅) = 𝑠)
2019elv 3441 . . . . . . . . . . . . . . . 16 ((rec((𝑦 ∈ V ↦ (𝑔‘{𝑧𝑦𝑥𝑧})), 𝑠) ↾ ω)‘∅) = 𝑠
2118, 20eqtri 2818 . . . . . . . . . . . . . . 15 (𝐹‘∅) = 𝑠
2221breq1i 4971 . . . . . . . . . . . . . 14 ((𝐹‘∅)𝑥𝑧𝑠𝑥𝑧)
2322biimpri 229 . . . . . . . . . . . . 13 (𝑠𝑥𝑧 → (𝐹‘∅)𝑥𝑧)
2423eximi 1817 . . . . . . . . . . . 12 (∃𝑧 𝑠𝑥𝑧 → ∃𝑧(𝐹‘∅)𝑥𝑧)
25 peano1 7460 . . . . . . . . . . . . 13 ∅ ∈ ω
262axdclem 9790 . . . . . . . . . . . . 13 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘∅)𝑥𝑧) → (∅ ∈ ω → (𝐹‘∅)𝑥(𝐹‘suc ∅)))
2725, 26mpi 20 . . . . . . . . . . . 12 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘∅)𝑥𝑧) → (𝐹‘∅)𝑥(𝐹‘suc ∅))
2824, 27syl3an3 1158 . . . . . . . . . . 11 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧 𝑠𝑥𝑧) → (𝐹‘∅)𝑥(𝐹‘suc ∅))
29283com23 1119 . . . . . . . . . 10 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝐹‘∅)𝑥(𝐹‘suc ∅))
30 fvex 6554 . . . . . . . . . . . . . . . . 17 (𝐹𝑘) ∈ V
31 fvex 6554 . . . . . . . . . . . . . . . . 17 (𝐹‘suc 𝑘) ∈ V
3230, 31brelrn 5697 . . . . . . . . . . . . . . . 16 ((𝐹𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘) ∈ ran 𝑥)
33 ssel 3885 . . . . . . . . . . . . . . . 16 (ran 𝑥 ⊆ dom 𝑥 → ((𝐹‘suc 𝑘) ∈ ran 𝑥 → (𝐹‘suc 𝑘) ∈ dom 𝑥))
3432, 33syl5 34 . . . . . . . . . . . . . . 15 (ran 𝑥 ⊆ dom 𝑥 → ((𝐹𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘) ∈ dom 𝑥))
3531eldm 5658 . . . . . . . . . . . . . . 15 ((𝐹‘suc 𝑘) ∈ dom 𝑥 ↔ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧)
3634, 35syl6ib 252 . . . . . . . . . . . . . 14 (ran 𝑥 ⊆ dom 𝑥 → ((𝐹𝑘)𝑥(𝐹‘suc 𝑘) → ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧))
3736ad2antll 725 . . . . . . . . . . . . 13 ((𝑘 ∈ ω ∧ (∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹𝑘)𝑥(𝐹‘suc 𝑘) → ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧))
38 peano2 7461 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
392axdclem 9790 . . . . . . . . . . . . . . . . 17 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) → (suc 𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))
4038, 39syl5 34 . . . . . . . . . . . . . . . 16 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃𝑧(𝐹‘suc 𝑘)𝑥𝑧) → (𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))
41403expia 1114 . . . . . . . . . . . . . . 15 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝑘 ∈ ω → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))))
4241com3r 87 . . . . . . . . . . . . . 14 (𝑘 ∈ ω → ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))))
4342imp 407 . . . . . . . . . . . . 13 ((𝑘 ∈ ω ∧ (∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → (∃𝑧(𝐹‘suc 𝑘)𝑥𝑧 → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))
4437, 43syld 47 . . . . . . . . . . . 12 ((𝑘 ∈ ω ∧ (∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))
45443adantr2 1163 . . . . . . . . . . 11 ((𝑘 ∈ ω ∧ (∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥)) → ((𝐹𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘)))
4645ex 413 . . . . . . . . . 10 (𝑘 ∈ ω → ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ((𝐹𝑘)𝑥(𝐹‘suc 𝑘) → (𝐹‘suc 𝑘)𝑥(𝐹‘suc suc 𝑘))))
479, 13, 17, 29, 46finds2 7469 . . . . . . . . 9 (𝑛 ∈ ω → ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝐹𝑛)𝑥(𝐹‘suc 𝑛)))
4847com12 32 . . . . . . . 8 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝑛 ∈ ω → (𝐹𝑛)𝑥(𝐹‘suc 𝑛)))
49 fvex 6554 . . . . . . . . 9 (𝐹𝑛) ∈ V
50 fvex 6554 . . . . . . . . 9 (𝐹‘suc 𝑛) ∈ V
5149, 50breldm 5666 . . . . . . . 8 ((𝐹𝑛)𝑥(𝐹‘suc 𝑛) → (𝐹𝑛) ∈ dom 𝑥)
5248, 51syl6 35 . . . . . . 7 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → (𝑛 ∈ ω → (𝐹𝑛) ∈ dom 𝑥))
5352ralrimiv 3147 . . . . . 6 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∀𝑛 ∈ ω (𝐹𝑛) ∈ dom 𝑥)
54 ffnfv 6748 . . . . . 6 (𝐹:ω⟶dom 𝑥 ↔ (𝐹 Fn ω ∧ ∀𝑛 ∈ ω (𝐹𝑛) ∈ dom 𝑥))
555, 53, 54sylanbrc 583 . . . . 5 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹:ω⟶dom 𝑥)
56 omex 8955 . . . . . 6 ω ∈ V
5756a1i 11 . . . . 5 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ω ∈ V)
58 vex 3439 . . . . . . 7 𝑥 ∈ V
5958dmex 7475 . . . . . 6 dom 𝑥 ∈ V
6059a1i 11 . . . . 5 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → dom 𝑥 ∈ V)
61 fex2 7497 . . . . 5 ((𝐹:ω⟶dom 𝑥 ∧ ω ∈ V ∧ dom 𝑥 ∈ V) → 𝐹 ∈ V)
6255, 57, 60, 61syl3anc 1364 . . . 4 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → 𝐹 ∈ V)
6348ralrimiv 3147 . . . 4 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∀𝑛 ∈ ω (𝐹𝑛)𝑥(𝐹‘suc 𝑛))
64 fveq1 6540 . . . . . 6 (𝑓 = 𝐹 → (𝑓𝑛) = (𝐹𝑛))
65 fveq1 6540 . . . . . 6 (𝑓 = 𝐹 → (𝑓‘suc 𝑛) = (𝐹‘suc 𝑛))
6664, 65breq12d 4977 . . . . 5 (𝑓 = 𝐹 → ((𝑓𝑛)𝑥(𝑓‘suc 𝑛) ↔ (𝐹𝑛)𝑥(𝐹‘suc 𝑛)))
6766ralbidv 3163 . . . 4 (𝑓 = 𝐹 → (∀𝑛 ∈ ω (𝑓𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∀𝑛 ∈ ω (𝐹𝑛)𝑥(𝐹‘suc 𝑛)))
6862, 63, 67elabd 3605 . . 3 ((∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ ∃𝑧 𝑠𝑥𝑧 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓𝑛 ∈ ω (𝑓𝑛)𝑥(𝑓‘suc 𝑛))
69683exp 1112 . 2 (∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) → (∃𝑧 𝑠𝑥𝑧 → (ran 𝑥 ⊆ dom 𝑥 → ∃𝑓𝑛 ∈ ω (𝑓𝑛)𝑥(𝑓‘suc 𝑛))))
7059pwex 5175 . . 3 𝒫 dom 𝑥 ∈ V
7170ac4c 9747 . 2 𝑔𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)
7269, 71exlimiiv 1910 1 (∃𝑧 𝑠𝑥𝑧 → (ran 𝑥 ⊆ dom 𝑥 → ∃𝑓𝑛 ∈ ω (𝑓𝑛)𝑥(𝑓‘suc 𝑛)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1080   = wceq 1522  wex 1762  wcel 2080  {cab 2774  wne 2983  wral 3104  Vcvv 3436  wss 3861  c0 4213  𝒫 cpw 4455   class class class wbr 4964  cmpt 5043  dom cdm 5446  ran crn 5447  cres 5448  suc csuc 6071   Fn wfn 6223  wf 6224  cfv 6228  ωcom 7439  reccrdg 7900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-rep 5084  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322  ax-inf2 8953  ax-ac2 9734
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-ral 3109  df-rex 3110  df-reu 3111  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-pss 3878  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-tp 4479  df-op 4481  df-uni 4748  df-iun 4829  df-br 4965  df-opab 5027  df-mpt 5044  df-tr 5067  df-id 5351  df-eprel 5356  df-po 5365  df-so 5366  df-fr 5405  df-we 5407  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-pred 6026  df-ord 6072  df-on 6073  df-lim 6074  df-suc 6075  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-fv 6236  df-om 7440  df-wrecs 7801  df-recs 7863  df-rdg 7901  df-ac 9391
This theorem is referenced by:  axdc  9792
  Copyright terms: Public domain W3C validator