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