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

Theorem ismkvnnlem 13465
 Description: Lemma for ismkvnn 13466. The result, with a hypothesis to give a name to an expression for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
Hypothesis
Ref Expression
ismkvnnlem.g 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
Assertion
Ref Expression
ismkvnnlem (𝐴𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)))
Distinct variable groups:   𝐴,𝑓,𝑥   𝑓,𝐺,𝑥   𝑓,𝑉,𝑥

Proof of Theorem ismkvnnlem
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 ismkvmap 7045 . 2 (𝐴𝑉 → (𝐴 ∈ Markov ↔ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)))
2 nfv 1509 . . . . . . . . 9 𝑥 𝐴𝑉
3 nfcv 2282 . . . . . . . . . 10 𝑥(2o𝑚 𝐴)
4 nfra1 2470 . . . . . . . . . . . 12 𝑥𝑥𝐴 (𝑔𝑥) = 1o
54nfn 1637 . . . . . . . . . . 11 𝑥 ¬ ∀𝑥𝐴 (𝑔𝑥) = 1o
6 nfre1 2480 . . . . . . . . . . 11 𝑥𝑥𝐴 (𝑔𝑥) = ∅
75, 6nfim 1552 . . . . . . . . . 10 𝑥(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)
83, 7nfralxy 2475 . . . . . . . . 9 𝑥𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)
92, 8nfan 1545 . . . . . . . 8 𝑥(𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅))
10 nfv 1509 . . . . . . . 8 𝑥 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)
119, 10nfan 1545 . . . . . . 7 𝑥((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴))
12 ismkvnnlem.g . . . . . . . . . . . 12 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
1312frechashgf1o 10259 . . . . . . . . . . 11 𝐺:ω–1-1-onto→ℕ0
14 0nn0 9043 . . . . . . . . . . . . 13 0 ∈ ℕ0
15 1nn0 9044 . . . . . . . . . . . . 13 1 ∈ ℕ0
16 prssi 3687 . . . . . . . . . . . . 13 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
1714, 15, 16mp2an 423 . . . . . . . . . . . 12 {0, 1} ⊆ ℕ0
18 elmapi 6575 . . . . . . . . . . . . . 14 (𝑓 ∈ ({0, 1} ↑𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
1918ad2antlr 481 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑓:𝐴⟶{0, 1})
20 simpr 109 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑥𝐴)
2119, 20ffvelrnd 5567 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ {0, 1})
2217, 21sseldi 3101 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℕ0)
23 f1ocnvfv2 5690 . . . . . . . . . . 11 ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑓𝑥) ∈ ℕ0) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝑓𝑥))
2413, 22, 23sylancr 411 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝑓𝑥))
2524adantr 274 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝑓𝑥))
26 fvco3 5503 . . . . . . . . . . . . . 14 ((𝑓:𝐴⟶{0, 1} ∧ 𝑥𝐴) → ((𝐺𝑓)‘𝑥) = (𝐺‘(𝑓𝑥)))
2719, 26sylancom 417 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝐺𝑓)‘𝑥) = (𝐺‘(𝑓𝑥)))
2827adantr 274 . . . . . . . . . . . 12 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → ((𝐺𝑓)‘𝑥) = (𝐺‘(𝑓𝑥)))
29 simpr 109 . . . . . . . . . . . 12 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → ((𝐺𝑓)‘𝑥) = 1o)
3028, 29eqtr3d 2175 . . . . . . . . . . 11 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝐺‘(𝑓𝑥)) = 1o)
3130fveq2d 5436 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝐺‘1o))
32 df-1o 6324 . . . . . . . . . . . 12 1o = suc ∅
3332fveq2i 5435 . . . . . . . . . . 11 (𝐺‘1o) = (𝐺‘suc ∅)
34 0zd 9117 . . . . . . . . . . . . 13 (⊤ → 0 ∈ ℤ)
35 peano1 4518 . . . . . . . . . . . . . 14 ∅ ∈ ω
3635a1i 9 . . . . . . . . . . . . 13 (⊤ → ∅ ∈ ω)
3734, 12, 36frec2uzsucd 10232 . . . . . . . . . . . 12 (⊤ → (𝐺‘suc ∅) = ((𝐺‘∅) + 1))
3837mptru 1341 . . . . . . . . . . 11 (𝐺‘suc ∅) = ((𝐺‘∅) + 1)
3934, 12frec2uz0d 10230 . . . . . . . . . . . . . 14 (⊤ → (𝐺‘∅) = 0)
4039mptru 1341 . . . . . . . . . . . . 13 (𝐺‘∅) = 0
4140oveq1i 5795 . . . . . . . . . . . 12 ((𝐺‘∅) + 1) = (0 + 1)
42 0p1e1 8885 . . . . . . . . . . . 12 (0 + 1) = 1
4341, 42eqtri 2161 . . . . . . . . . . 11 ((𝐺‘∅) + 1) = 1
4433, 38, 433eqtri 2165 . . . . . . . . . 10 (𝐺‘1o) = 1
4531, 44eqtrdi 2189 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝐺‘(𝐺‘(𝑓𝑥))) = 1)
4625, 45eqtr3d 2175 . . . . . . . 8 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝑓𝑥) = 1)
4746ex 114 . . . . . . 7 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑓)‘𝑥) = 1o → (𝑓𝑥) = 1))
4811, 47ralimdaa 2502 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o → ∀𝑥𝐴 (𝑓𝑥) = 1))
4948con3d 621 . . . . 5 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ¬ ∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o))
50 fveq1 5431 . . . . . . . . . 10 (𝑔 = (𝐺𝑓) → (𝑔𝑥) = ((𝐺𝑓)‘𝑥))
5150eqeq1d 2149 . . . . . . . . 9 (𝑔 = (𝐺𝑓) → ((𝑔𝑥) = 1o ↔ ((𝐺𝑓)‘𝑥) = 1o))
5251ralbidv 2439 . . . . . . . 8 (𝑔 = (𝐺𝑓) → (∀𝑥𝐴 (𝑔𝑥) = 1o ↔ ∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o))
5352notbid 657 . . . . . . 7 (𝑔 = (𝐺𝑓) → (¬ ∀𝑥𝐴 (𝑔𝑥) = 1o ↔ ¬ ∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o))
5450eqeq1d 2149 . . . . . . . 8 (𝑔 = (𝐺𝑓) → ((𝑔𝑥) = ∅ ↔ ((𝐺𝑓)‘𝑥) = ∅))
5554rexbidv 2440 . . . . . . 7 (𝑔 = (𝐺𝑓) → (∃𝑥𝐴 (𝑔𝑥) = ∅ ↔ ∃𝑥𝐴 ((𝐺𝑓)‘𝑥) = ∅))
5653, 55imbi12d 233 . . . . . 6 (𝑔 = (𝐺𝑓) → ((¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅) ↔ (¬ ∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o → ∃𝑥𝐴 ((𝐺𝑓)‘𝑥) = ∅)))
57 simplr 520 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅))
5812012of 13406 . . . . . . . 8 (𝐺 ↾ {0, 1}):{0, 1}⟶2o
5918adantl 275 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝑓:𝐴⟶{0, 1})
60 fco2 5300 . . . . . . . 8 (((𝐺 ↾ {0, 1}):{0, 1}⟶2o𝑓:𝐴⟶{0, 1}) → (𝐺𝑓):𝐴⟶2o)
6158, 59, 60sylancr 411 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝐺𝑓):𝐴⟶2o)
62 2onn 6428 . . . . . . . . 9 2o ∈ ω
6362a1i 9 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 2o ∈ ω)
64 simpll 519 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝐴𝑉)
6563, 64elmapd 6567 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ((𝐺𝑓) ∈ (2o𝑚 𝐴) ↔ (𝐺𝑓):𝐴⟶2o))
6661, 65mpbird 166 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝐺𝑓) ∈ (2o𝑚 𝐴))
6756, 57, 66rspcdva 2799 . . . . 5 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (¬ ∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o → ∃𝑥𝐴 ((𝐺𝑓)‘𝑥) = ∅))
6824adantr 274 . . . . . . . 8 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝑓𝑥))
6927eqeq1d 2149 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑓)‘𝑥) = ∅ ↔ (𝐺‘(𝑓𝑥)) = ∅))
7069biimpa 294 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝐺‘(𝑓𝑥)) = ∅)
7170fveq2d 5436 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝐺‘∅))
7271, 40eqtrdi 2189 . . . . . . . 8 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝐺‘(𝐺‘(𝑓𝑥))) = 0)
7368, 72eqtr3d 2175 . . . . . . 7 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝑓𝑥) = 0)
7473exp31 362 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝑥𝐴 → (((𝐺𝑓)‘𝑥) = ∅ → (𝑓𝑥) = 0)))
7511, 74reximdai 2534 . . . . 5 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∃𝑥𝐴 ((𝐺𝑓)‘𝑥) = ∅ → ∃𝑥𝐴 (𝑓𝑥) = 0))
7649, 67, 753syld 57 . . . 4 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0))
7776ralrimiva 2509 . . 3 ((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0))
78 nfcv 2282 . . . . . . . . . 10 𝑥({0, 1} ↑𝑚 𝐴)
79 nfra1 2470 . . . . . . . . . . . 12 𝑥𝑥𝐴 (𝑓𝑥) = 1
8079nfn 1637 . . . . . . . . . . 11 𝑥 ¬ ∀𝑥𝐴 (𝑓𝑥) = 1
81 nfre1 2480 . . . . . . . . . . 11 𝑥𝑥𝐴 (𝑓𝑥) = 0
8280, 81nfim 1552 . . . . . . . . . 10 𝑥(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)
8378, 82nfralxy 2475 . . . . . . . . 9 𝑥𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)
842, 83nfan 1545 . . . . . . . 8 𝑥(𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0))
85 nfv 1509 . . . . . . . 8 𝑥 𝑔 ∈ (2o𝑚 𝐴)
8684, 85nfan 1545 . . . . . . 7 𝑥((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴))
87 elmapi 6575 . . . . . . . . . . . . . 14 (𝑔 ∈ (2o𝑚 𝐴) → 𝑔:𝐴⟶2o)
8887ad2antlr 481 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑔:𝐴⟶2o)
89 omelon 4533 . . . . . . . . . . . . . . . 16 ω ∈ On
9089onelssi 4361 . . . . . . . . . . . . . . 15 (2o ∈ ω → 2o ⊆ ω)
9162, 90ax-mp 5 . . . . . . . . . . . . . 14 2o ⊆ ω
9291a1i 9 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 2o ⊆ ω)
9388, 92fssd 5296 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑔:𝐴⟶ω)
94 simpr 109 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑥𝐴)
9593, 94ffvelrnd 5567 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑔𝑥) ∈ ω)
96 f1ocnvfv1 5689 . . . . . . . . . . 11 ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑔𝑥) ∈ ω) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝑔𝑥))
9713, 95, 96sylancr 411 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝑔𝑥))
9897adantr 274 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝑔𝑥))
99 fvco3 5503 . . . . . . . . . . . . . 14 ((𝑔:𝐴⟶2o𝑥𝐴) → ((𝐺𝑔)‘𝑥) = (𝐺‘(𝑔𝑥)))
10088, 99sylancom 417 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝐺𝑔)‘𝑥) = (𝐺‘(𝑔𝑥)))
101100eqeq1d 2149 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔𝑥)) = 1))
102101biimpa 294 . . . . . . . . . . 11 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝐺‘(𝑔𝑥)) = 1)
103102fveq2d 5436 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝐺‘1))
104 1onn 6427 . . . . . . . . . . . 12 1o ∈ ω
105 f1ocnvfv 5691 . . . . . . . . . . . 12 ((𝐺:ω–1-1-onto→ℕ0 ∧ 1o ∈ ω) → ((𝐺‘1o) = 1 → (𝐺‘1) = 1o))
10613, 104, 105mp2an 423 . . . . . . . . . . 11 ((𝐺‘1o) = 1 → (𝐺‘1) = 1o)
10744, 106ax-mp 5 . . . . . . . . . 10 (𝐺‘1) = 1o
108103, 107eqtrdi 2189 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝐺‘(𝐺‘(𝑔𝑥))) = 1o)
10998, 108eqtr3d 2175 . . . . . . . 8 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝑔𝑥) = 1o)
110109ex 114 . . . . . . 7 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑔)‘𝑥) = 1 → (𝑔𝑥) = 1o))
11186, 110ralimdaa 2502 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1 → ∀𝑥𝐴 (𝑔𝑥) = 1o))
112111con3d 621 . . . . 5 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ¬ ∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1))
113 fveq1 5431 . . . . . . . . . 10 (𝑓 = (𝐺𝑔) → (𝑓𝑥) = ((𝐺𝑔)‘𝑥))
114113eqeq1d 2149 . . . . . . . . 9 (𝑓 = (𝐺𝑔) → ((𝑓𝑥) = 1 ↔ ((𝐺𝑔)‘𝑥) = 1))
115114ralbidv 2439 . . . . . . . 8 (𝑓 = (𝐺𝑔) → (∀𝑥𝐴 (𝑓𝑥) = 1 ↔ ∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1))
116115notbid 657 . . . . . . 7 (𝑓 = (𝐺𝑔) → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1 ↔ ¬ ∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1))
117113eqeq1d 2149 . . . . . . . 8 (𝑓 = (𝐺𝑔) → ((𝑓𝑥) = 0 ↔ ((𝐺𝑔)‘𝑥) = 0))
118117rexbidv 2440 . . . . . . 7 (𝑓 = (𝐺𝑔) → (∃𝑥𝐴 (𝑓𝑥) = 0 ↔ ∃𝑥𝐴 ((𝐺𝑔)‘𝑥) = 0))
119116, 118imbi12d 233 . . . . . 6 (𝑓 = (𝐺𝑔) → ((¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0) ↔ (¬ ∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1 → ∃𝑥𝐴 ((𝐺𝑔)‘𝑥) = 0)))
120 simplr 520 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0))
121122o01f 13407 . . . . . . . 8 (𝐺 ↾ 2o):2o⟶{0, 1}
12287adantl 275 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → 𝑔:𝐴⟶2o)
123 fco2 5300 . . . . . . . 8 (((𝐺 ↾ 2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺𝑔):𝐴⟶{0, 1})
124121, 122, 123sylancr 411 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝐺𝑔):𝐴⟶{0, 1})
125 prexg 4143 . . . . . . . . . 10 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ∈ V)
12614, 15, 125mp2an 423 . . . . . . . . 9 {0, 1} ∈ V
127126a1i 9 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → {0, 1} ∈ V)
128 simpll 519 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → 𝐴𝑉)
129127, 128elmapd 6567 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → ((𝐺𝑔) ∈ ({0, 1} ↑𝑚 𝐴) ↔ (𝐺𝑔):𝐴⟶{0, 1}))
130124, 129mpbird 166 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝐺𝑔) ∈ ({0, 1} ↑𝑚 𝐴))
131119, 120, 130rspcdva 2799 . . . . 5 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (¬ ∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1 → ∃𝑥𝐴 ((𝐺𝑔)‘𝑥) = 0))
13297adantr 274 . . . . . . . 8 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝑔𝑥))
133100eqeq1d 2149 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑔)‘𝑥) = 0 ↔ (𝐺‘(𝑔𝑥)) = 0))
134133biimpa 294 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝐺‘(𝑔𝑥)) = 0)
135134fveq2d 5436 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝐺‘0))
136 f1ocnvfv 5691 . . . . . . . . . . 11 ((𝐺:ω–1-1-onto→ℕ0 ∧ ∅ ∈ ω) → ((𝐺‘∅) = 0 → (𝐺‘0) = ∅))
13713, 35, 136mp2an 423 . . . . . . . . . 10 ((𝐺‘∅) = 0 → (𝐺‘0) = ∅)
13840, 137ax-mp 5 . . . . . . . . 9 (𝐺‘0) = ∅
139135, 138eqtrdi 2189 . . . . . . . 8 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝐺‘(𝐺‘(𝑔𝑥))) = ∅)
140132, 139eqtr3d 2175 . . . . . . 7 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝑔𝑥) = ∅)
141140exp31 362 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝑥𝐴 → (((𝐺𝑔)‘𝑥) = 0 → (𝑔𝑥) = ∅)))
14286, 141reximdai 2534 . . . . 5 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∃𝑥𝐴 ((𝐺𝑔)‘𝑥) = 0 → ∃𝑥𝐴 (𝑔𝑥) = ∅))
143112, 131, 1423syld 57 . . . 4 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅))
144143ralrimiva 2509 . . 3 ((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)) → ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅))
14577, 144impbida 586 . 2 (𝐴𝑉 → (∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅) ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)))
1461, 145bitrd 187 1 (𝐴𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332  ⊤wtru 1333   ∈ wcel 1481  ∀wral 2417  ∃wrex 2418  Vcvv 2690   ⊆ wss 3077  ∅c0 3369  {cpr 3534   ↦ cmpt 3998  suc csuc 4297  ωcom 4514  ◡ccnv 4549   ↾ cres 4552   ∘ ccom 4554  ⟶wf 5130  –1-1-onto→wf1o 5133  ‘cfv 5134  (class class class)co 5785  freccfrec 6298  1oc1o 6317  2oc2o 6318   ↑𝑚 cmap 6553  Markovcmarkov 7042  0cc0 7671  1c1 7672   + caddc 7674  ℕ0cn0 9028  ℤcz 9105 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 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4052  ax-sep 4055  ax-nul 4063  ax-pow 4107  ax-pr 4141  ax-un 4365  ax-setind 4462  ax-iinf 4512  ax-cnex 7762  ax-resscn 7763  ax-1cn 7764  ax-1re 7765  ax-icn 7766  ax-addcl 7767  ax-addrcl 7768  ax-mulcl 7769  ax-addcom 7771  ax-addass 7773  ax-distr 7775  ax-i2m1 7776  ax-0lt1 7777  ax-0id 7779  ax-rnegex 7780  ax-cnre 7782  ax-pre-ltirr 7783  ax-pre-ltwlin 7784  ax-pre-lttrn 7785  ax-pre-ltadd 7787 This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-int 3781  df-iun 3824  df-br 3939  df-opab 3999  df-mpt 4000  df-tr 4036  df-id 4225  df-iord 4298  df-on 4300  df-ilim 4301  df-suc 4303  df-iom 4515  df-xp 4556  df-rel 4557  df-cnv 4558  df-co 4559  df-dm 4560  df-rn 4561  df-res 4562  df-ima 4563  df-iota 5099  df-fun 5136  df-fn 5137  df-f 5138  df-f1 5139  df-fo 5140  df-f1o 5141  df-fv 5142  df-riota 5741  df-ov 5788  df-oprab 5789  df-mpo 5790  df-recs 6213  df-frec 6299  df-1o 6324  df-2o 6325  df-map 6555  df-markov 7043  df-pnf 7853  df-mnf 7854  df-xr 7855  df-ltxr 7856  df-le 7857  df-sub 7986  df-neg 7987  df-inn 8772  df-n0 9029  df-z 9106  df-uz 9378 This theorem is referenced by:  ismkvnn  13466
 Copyright terms: Public domain W3C validator