Mathbox for Jim Kingdon < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  iswomninnlem GIF version

Theorem iswomninnlem 13463
 Description: Lemma for iswomnimap 7059. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.)
Hypothesis
Ref Expression
iswomninnlem.g 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
Assertion
Ref Expression
iswomninnlem (𝐴𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1))
Distinct variable groups:   𝐴,𝑓,𝑥   𝑓,𝐺,𝑥   𝑓,𝑉,𝑥

Proof of Theorem iswomninnlem
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 iswomnimap 7059 . 2 (𝐴𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o))
2 fveq1 5432 . . . . . . . . 9 (𝑔 = (𝐺𝑓) → (𝑔𝑥) = ((𝐺𝑓)‘𝑥))
32eqeq1d 2150 . . . . . . . 8 (𝑔 = (𝐺𝑓) → ((𝑔𝑥) = 1o ↔ ((𝐺𝑓)‘𝑥) = 1o))
43ralbidv 2440 . . . . . . 7 (𝑔 = (𝐺𝑓) → (∀𝑥𝐴 (𝑔𝑥) = 1o ↔ ∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o))
54dcbid 824 . . . . . 6 (𝑔 = (𝐺𝑓) → (DECID𝑥𝐴 (𝑔𝑥) = 1oDECID𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o))
6 simplr 520 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o)
7 iswomninnlem.g . . . . . . . . . . 11 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
87012of 13407 . . . . . . . . . 10 (𝐺 ↾ {0, 1}):{0, 1}⟶2o
9 elmapi 6576 . . . . . . . . . 10 (𝑓 ∈ ({0, 1} ↑𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
10 fco2 5301 . . . . . . . . . 10 (((𝐺 ↾ {0, 1}):{0, 1}⟶2o𝑓:𝐴⟶{0, 1}) → (𝐺𝑓):𝐴⟶2o)
118, 9, 10sylancr 411 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑𝑚 𝐴) → (𝐺𝑓):𝐴⟶2o)
1211adantl 275 . . . . . . . 8 ((𝐴𝑉𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝐺𝑓):𝐴⟶2o)
13 2onn 6429 . . . . . . . . . 10 2o ∈ ω
1413a1i 9 . . . . . . . . 9 ((𝐴𝑉𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 2o ∈ ω)
15 simpl 108 . . . . . . . . 9 ((𝐴𝑉𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝐴𝑉)
1614, 15elmapd 6568 . . . . . . . 8 ((𝐴𝑉𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ((𝐺𝑓) ∈ (2o𝑚 𝐴) ↔ (𝐺𝑓):𝐴⟶2o))
1712, 16mpbird 166 . . . . . . 7 ((𝐴𝑉𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝐺𝑓) ∈ (2o𝑚 𝐴))
1817adantlr 469 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝐺𝑓) ∈ (2o𝑚 𝐴))
195, 6, 18rspcdva 2800 . . . . 5 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → DECID𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o)
20 nfv 1505 . . . . . . . . 9 𝑥 𝐴𝑉
21 nfcv 2283 . . . . . . . . . 10 𝑥(2o𝑚 𝐴)
22 nfra1 2471 . . . . . . . . . . 11 𝑥𝑥𝐴 (𝑔𝑥) = 1o
2322nfdc 1635 . . . . . . . . . 10 𝑥DECID𝑥𝐴 (𝑔𝑥) = 1o
2421, 23nfralxy 2476 . . . . . . . . 9 𝑥𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o
2520, 24nfan 1541 . . . . . . . 8 𝑥(𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o)
26 nfv 1505 . . . . . . . 8 𝑥 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)
2725, 26nfan 1541 . . . . . . 7 𝑥((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴))
289ad2antlr 481 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑓:𝐴⟶{0, 1})
29 fvco3 5504 . . . . . . . . . 10 ((𝑓:𝐴⟶{0, 1} ∧ 𝑥𝐴) → ((𝐺𝑓)‘𝑥) = (𝐺‘(𝑓𝑥)))
3028, 29sylancom 417 . . . . . . . . 9 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝐺𝑓)‘𝑥) = (𝐺‘(𝑓𝑥)))
3130eqeq1d 2150 . . . . . . . 8 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑓)‘𝑥) = 1o ↔ (𝐺‘(𝑓𝑥)) = 1o))
32 df-1o 6325 . . . . . . . . . . . 12 1o = suc ∅
3332fveq2i 5436 . . . . . . . . . . 11 (𝐺‘1o) = (𝐺‘suc ∅)
34 0zd 9119 . . . . . . . . . . . . 13 (⊤ → 0 ∈ ℤ)
35 peano1 4519 . . . . . . . . . . . . . 14 ∅ ∈ ω
3635a1i 9 . . . . . . . . . . . . 13 (⊤ → ∅ ∈ ω)
3734, 7, 36frec2uzsucd 10234 . . . . . . . . . . . 12 (⊤ → (𝐺‘suc ∅) = ((𝐺‘∅) + 1))
3837mptru 1341 . . . . . . . . . . 11 (𝐺‘suc ∅) = ((𝐺‘∅) + 1)
3934, 7frec2uz0d 10232 . . . . . . . . . . . . . 14 (⊤ → (𝐺‘∅) = 0)
4039mptru 1341 . . . . . . . . . . . . 13 (𝐺‘∅) = 0
4140oveq1i 5796 . . . . . . . . . . . 12 ((𝐺‘∅) + 1) = (0 + 1)
42 0p1e1 8887 . . . . . . . . . . . 12 (0 + 1) = 1
4341, 42eqtri 2162 . . . . . . . . . . 11 ((𝐺‘∅) + 1) = 1
4433, 38, 433eqtri 2166 . . . . . . . . . 10 (𝐺‘1o) = 1
4544eqeq2i 2152 . . . . . . . . 9 ((𝐺‘(𝐺‘(𝑓𝑥))) = (𝐺‘1o) ↔ (𝐺‘(𝐺‘(𝑓𝑥))) = 1)
467frechashgf1o 10261 . . . . . . . . . . . . 13 𝐺:ω–1-1-onto→ℕ0
47 f1ocnv 5392 . . . . . . . . . . . . 13 (𝐺:ω–1-1-onto→ℕ0𝐺:ℕ01-1-onto→ω)
48 f1of 5379 . . . . . . . . . . . . 13 (𝐺:ℕ01-1-onto→ω → 𝐺:ℕ0⟶ω)
4946, 47, 48mp2b 8 . . . . . . . . . . . 12 𝐺:ℕ0⟶ω
5049a1i 9 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → 𝐺:ℕ0⟶ω)
51 0nn0 9045 . . . . . . . . . . . . 13 0 ∈ ℕ0
52 1nn0 9046 . . . . . . . . . . . . 13 1 ∈ ℕ0
53 prssi 3688 . . . . . . . . . . . . 13 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
5451, 52, 53mp2an 423 . . . . . . . . . . . 12 {0, 1} ⊆ ℕ0
55 simpr 109 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑥𝐴)
5628, 55ffvelrnd 5568 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ {0, 1})
5754, 56sseldi 3102 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℕ0)
5850, 57ffvelrnd 5568 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (𝐺‘(𝑓𝑥)) ∈ ω)
59 1onn 6428 . . . . . . . . . . 11 1o ∈ ω
60 f1of1 5378 . . . . . . . . . . . . 13 (𝐺:ω–1-1-onto→ℕ0𝐺:ω–1-1→ℕ0)
6146, 60ax-mp 5 . . . . . . . . . . . 12 𝐺:ω–1-1→ℕ0
62 f1fveq 5685 . . . . . . . . . . . 12 ((𝐺:ω–1-1→ℕ0 ∧ ((𝐺‘(𝑓𝑥)) ∈ ω ∧ 1o ∈ ω)) → ((𝐺‘(𝐺‘(𝑓𝑥))) = (𝐺‘1o) ↔ (𝐺‘(𝑓𝑥)) = 1o))
6361, 62mpan 421 . . . . . . . . . . 11 (((𝐺‘(𝑓𝑥)) ∈ ω ∧ 1o ∈ ω) → ((𝐺‘(𝐺‘(𝑓𝑥))) = (𝐺‘1o) ↔ (𝐺‘(𝑓𝑥)) = 1o))
6459, 63mpan2 422 . . . . . . . . . 10 ((𝐺‘(𝑓𝑥)) ∈ ω → ((𝐺‘(𝐺‘(𝑓𝑥))) = (𝐺‘1o) ↔ (𝐺‘(𝑓𝑥)) = 1o))
6558, 64syl 14 . . . . . . . . 9 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝐺‘(𝐺‘(𝑓𝑥))) = (𝐺‘1o) ↔ (𝐺‘(𝑓𝑥)) = 1o))
6645, 65bitr3id 193 . . . . . . . 8 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝐺‘(𝐺‘(𝑓𝑥))) = 1 ↔ (𝐺‘(𝑓𝑥)) = 1o))
67 f1ocnvfv2 5691 . . . . . . . . . 10 ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑓𝑥) ∈ ℕ0) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝑓𝑥))
6846, 57, 67sylancr 411 . . . . . . . . 9 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝑓𝑥))
6968eqeq1d 2150 . . . . . . . 8 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝐺‘(𝐺‘(𝑓𝑥))) = 1 ↔ (𝑓𝑥) = 1))
7031, 66, 693bitr2d 215 . . . . . . 7 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑓)‘𝑥) = 1o ↔ (𝑓𝑥) = 1))
7127, 70ralbida 2434 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o ↔ ∀𝑥𝐴 (𝑓𝑥) = 1))
7271dcbid 824 . . . . 5 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (DECID𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1oDECID𝑥𝐴 (𝑓𝑥) = 1))
7319, 72mpbid 146 . . . 4 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → DECID𝑥𝐴 (𝑓𝑥) = 1)
7473ralrimiva 2510 . . 3 ((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1)
75 fveq1 5432 . . . . . . . . 9 (𝑓 = (𝐺𝑔) → (𝑓𝑥) = ((𝐺𝑔)‘𝑥))
7675eqeq1d 2150 . . . . . . . 8 (𝑓 = (𝐺𝑔) → ((𝑓𝑥) = 1 ↔ ((𝐺𝑔)‘𝑥) = 1))
7776ralbidv 2440 . . . . . . 7 (𝑓 = (𝐺𝑔) → (∀𝑥𝐴 (𝑓𝑥) = 1 ↔ ∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1))
7877dcbid 824 . . . . . 6 (𝑓 = (𝐺𝑔) → (DECID𝑥𝐴 (𝑓𝑥) = 1 ↔ DECID𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1))
79 simplr 520 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1)
8072o01f 13408 . . . . . . . 8 (𝐺 ↾ 2o):2o⟶{0, 1}
81 elmapi 6576 . . . . . . . . 9 (𝑔 ∈ (2o𝑚 𝐴) → 𝑔:𝐴⟶2o)
8281adantl 275 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → 𝑔:𝐴⟶2o)
83 fco2 5301 . . . . . . . 8 (((𝐺 ↾ 2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺𝑔):𝐴⟶{0, 1})
8480, 82, 83sylancr 411 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝐺𝑔):𝐴⟶{0, 1})
85 prexg 4144 . . . . . . . . . 10 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ∈ V)
8651, 52, 85mp2an 423 . . . . . . . . 9 {0, 1} ∈ V
8786a1i 9 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → {0, 1} ∈ V)
88 simpll 519 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → 𝐴𝑉)
8987, 88elmapd 6568 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → ((𝐺𝑔) ∈ ({0, 1} ↑𝑚 𝐴) ↔ (𝐺𝑔):𝐴⟶{0, 1}))
9084, 89mpbird 166 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝐺𝑔) ∈ ({0, 1} ↑𝑚 𝐴))
9178, 79, 90rspcdva 2800 . . . . 5 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → DECID𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1)
92 nfcv 2283 . . . . . . . . . 10 𝑥({0, 1} ↑𝑚 𝐴)
93 nfra1 2471 . . . . . . . . . . 11 𝑥𝑥𝐴 (𝑓𝑥) = 1
9493nfdc 1635 . . . . . . . . . 10 𝑥DECID𝑥𝐴 (𝑓𝑥) = 1
9592, 94nfralxy 2476 . . . . . . . . 9 𝑥𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1
9620, 95nfan 1541 . . . . . . . 8 𝑥(𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1)
97 nfv 1505 . . . . . . . 8 𝑥 𝑔 ∈ (2o𝑚 𝐴)
9896, 97nfan 1541 . . . . . . 7 𝑥((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴))
9981ad2antlr 481 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑔:𝐴⟶2o)
100 fvco3 5504 . . . . . . . . . 10 ((𝑔:𝐴⟶2o𝑥𝐴) → ((𝐺𝑔)‘𝑥) = (𝐺‘(𝑔𝑥)))
10199, 100sylancom 417 . . . . . . . . 9 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝐺𝑔)‘𝑥) = (𝐺‘(𝑔𝑥)))
102101eqeq1d 2150 . . . . . . . 8 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔𝑥)) = 1))
103 f1of 5379 . . . . . . . . . . 11 (𝐺:ω–1-1-onto→ℕ0𝐺:ω⟶ℕ0)
10446, 103mp1i 10 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝐺:ω⟶ℕ0)
105 omelon 4534 . . . . . . . . . . . . . 14 ω ∈ On
106105onelssi 4362 . . . . . . . . . . . . 13 (2o ∈ ω → 2o ⊆ ω)
10713, 106mp1i 10 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 2o ⊆ ω)
10899, 107fssd 5297 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑔:𝐴⟶ω)
109 simpr 109 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑥𝐴)
110108, 109ffvelrnd 5568 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑔𝑥) ∈ ω)
111104, 110ffvelrnd 5568 . . . . . . . . 9 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝐺‘(𝑔𝑥)) ∈ ℕ0)
112 f1ocnvfv 5692 . . . . . . . . . . . . 13 ((𝐺:ω–1-1-onto→ℕ0 ∧ 1o ∈ ω) → ((𝐺‘1o) = 1 → (𝐺‘1) = 1o))
11346, 59, 112mp2an 423 . . . . . . . . . . . 12 ((𝐺‘1o) = 1 → (𝐺‘1) = 1o)
11444, 113ax-mp 5 . . . . . . . . . . 11 (𝐺‘1) = 1o
115114eqeq2i 2152 . . . . . . . . . 10 ((𝐺‘(𝐺‘(𝑔𝑥))) = (𝐺‘1) ↔ (𝐺‘(𝐺‘(𝑔𝑥))) = 1o)
116 f1of1 5378 . . . . . . . . . . . . 13 (𝐺:ℕ01-1-onto→ω → 𝐺:ℕ01-1→ω)
11746, 47, 116mp2b 8 . . . . . . . . . . . 12 𝐺:ℕ01-1→ω
118 f1fveq 5685 . . . . . . . . . . . 12 ((𝐺:ℕ01-1→ω ∧ ((𝐺‘(𝑔𝑥)) ∈ ℕ0 ∧ 1 ∈ ℕ0)) → ((𝐺‘(𝐺‘(𝑔𝑥))) = (𝐺‘1) ↔ (𝐺‘(𝑔𝑥)) = 1))
119117, 118mpan 421 . . . . . . . . . . 11 (((𝐺‘(𝑔𝑥)) ∈ ℕ0 ∧ 1 ∈ ℕ0) → ((𝐺‘(𝐺‘(𝑔𝑥))) = (𝐺‘1) ↔ (𝐺‘(𝑔𝑥)) = 1))
12052, 119mpan2 422 . . . . . . . . . 10 ((𝐺‘(𝑔𝑥)) ∈ ℕ0 → ((𝐺‘(𝐺‘(𝑔𝑥))) = (𝐺‘1) ↔ (𝐺‘(𝑔𝑥)) = 1))
121115, 120bitr3id 193 . . . . . . . . 9 ((𝐺‘(𝑔𝑥)) ∈ ℕ0 → ((𝐺‘(𝐺‘(𝑔𝑥))) = 1o ↔ (𝐺‘(𝑔𝑥)) = 1))
122111, 121syl 14 . . . . . . . 8 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝐺‘(𝐺‘(𝑔𝑥))) = 1o ↔ (𝐺‘(𝑔𝑥)) = 1))
123 f1ocnvfv1 5690 . . . . . . . . . 10 ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑔𝑥) ∈ ω) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝑔𝑥))
12446, 110, 123sylancr 411 . . . . . . . . 9 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝑔𝑥))
125124eqeq1d 2150 . . . . . . . 8 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝐺‘(𝐺‘(𝑔𝑥))) = 1o ↔ (𝑔𝑥) = 1o))
126102, 122, 1253bitr2d 215 . . . . . . 7 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑔)‘𝑥) = 1 ↔ (𝑔𝑥) = 1o))
12798, 126ralbida 2434 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1 ↔ ∀𝑥𝐴 (𝑔𝑥) = 1o))
128127dcbid 824 . . . . 5 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (DECID𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1 ↔ DECID𝑥𝐴 (𝑔𝑥) = 1o))
12991, 128mpbid 146 . . . 4 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → DECID𝑥𝐴 (𝑔𝑥) = 1o)
130129ralrimiva 2510 . . 3 ((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1) → ∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o)
13174, 130impbida 586 . 2 (𝐴𝑉 → (∀𝑔 ∈ (2o𝑚 𝐴)DECID𝑥𝐴 (𝑔𝑥) = 1o ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1))
1321, 131bitrd 187 1 (𝐴𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  DECID wdc 820   = wceq 1332  ⊤wtru 1333   ∈ wcel 2112  ∀wral 2418  Vcvv 2691   ⊆ wss 3078  ∅c0 3370  {cpr 3535   ↦ cmpt 3999  suc csuc 4298  ωcom 4515  ◡ccnv 4550   ↾ cres 4553   ∘ ccom 4555  ⟶wf 5131  –1-1→wf1 5132  –1-1-onto→wf1o 5134  ‘cfv 5135  (class class class)co 5786  freccfrec 6299  1oc1o 6318  2oc2o 6319   ↑𝑚 cmap 6554  WOmnicwomni 7056  0cc0 7673  1c1 7674   + caddc 7676  ℕ0cn0 9030  ℤcz 9107 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2114  ax-14 2115  ax-ext 2123  ax-coll 4053  ax-sep 4056  ax-nul 4064  ax-pow 4108  ax-pr 4142  ax-un 4366  ax-setind 4463  ax-iinf 4513  ax-cnex 7764  ax-resscn 7765  ax-1cn 7766  ax-1re 7767  ax-icn 7768  ax-addcl 7769  ax-addrcl 7770  ax-mulcl 7771  ax-addcom 7773  ax-addass 7775  ax-distr 7777  ax-i2m1 7778  ax-0lt1 7779  ax-0id 7781  ax-rnegex 7782  ax-cnre 7784  ax-pre-ltirr 7785  ax-pre-ltwlin 7786  ax-pre-lttrn 7787  ax-pre-ltadd 7789 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1732  df-eu 1993  df-mo 1994  df-clab 2128  df-cleq 2134  df-clel 2137  df-nfc 2272  df-ne 2311  df-nel 2406  df-ral 2423  df-rex 2424  df-reu 2425  df-rab 2427  df-v 2693  df-sbc 2916  df-csb 3010  df-dif 3080  df-un 3082  df-in 3084  df-ss 3091  df-nul 3371  df-pw 3519  df-sn 3540  df-pr 3541  df-op 3543  df-uni 3747  df-int 3782  df-iun 3825  df-br 3940  df-opab 4000  df-mpt 4001  df-tr 4037  df-id 4226  df-iord 4299  df-on 4301  df-ilim 4302  df-suc 4304  df-iom 4516  df-xp 4557  df-rel 4558  df-cnv 4559  df-co 4560  df-dm 4561  df-rn 4562  df-res 4563  df-ima 4564  df-iota 5100  df-fun 5137  df-fn 5138  df-f 5139  df-f1 5140  df-fo 5141  df-f1o 5142  df-fv 5143  df-riota 5742  df-ov 5789  df-oprab 5790  df-mpo 5791  df-recs 6214  df-frec 6300  df-1o 6325  df-2o 6326  df-map 6556  df-womni 7057  df-pnf 7855  df-mnf 7856  df-xr 7857  df-ltxr 7858  df-le 7859  df-sub 7988  df-neg 7989  df-inn 8774  df-n0 9031  df-z 9108  df-uz 9380 This theorem is referenced by:  iswomninn  13464
 Copyright terms: Public domain W3C validator