ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ismkvnex GIF version

Theorem ismkvnex 7147
Description: The predicate of being Markov stated in terms of double negation and comparison with 1o. (Contributed by Jim Kingdon, 29-Nov-2023.)
Assertion
Ref Expression
ismkvnex (𝐴𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)))
Distinct variable groups:   𝐴,𝑓,𝑥   𝑓,𝑉,𝑥

Proof of Theorem ismkvnex
Dummy variables 𝑔 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq1 5510 . . . . . . . . 9 (𝑔 = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) → (𝑔𝑥) = ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥))
21eqeq1d 2186 . . . . . . . 8 (𝑔 = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) → ((𝑔𝑥) = 1o ↔ ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o))
32ralbidv 2477 . . . . . . 7 (𝑔 = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) → (∀𝑥𝐴 (𝑔𝑥) = 1o ↔ ∀𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o))
43notbid 667 . . . . . 6 (𝑔 = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) → (¬ ∀𝑥𝐴 (𝑔𝑥) = 1o ↔ ¬ ∀𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o))
51eqeq1d 2186 . . . . . . 7 (𝑔 = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) → ((𝑔𝑥) = ∅ ↔ ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = ∅))
65rexbidv 2478 . . . . . 6 (𝑔 = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) → (∃𝑥𝐴 (𝑔𝑥) = ∅ ↔ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = ∅))
74, 6imbi12d 234 . . . . 5 (𝑔 = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) → ((¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅) ↔ (¬ ∀𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o → ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = ∅)))
8 elex 2748 . . . . . . 7 (𝐴 ∈ Markov → 𝐴 ∈ V)
9 ismkvmap 7146 . . . . . . . 8 (𝐴 ∈ V → (𝐴 ∈ Markov ↔ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)))
109biimpd 144 . . . . . . 7 (𝐴 ∈ V → (𝐴 ∈ Markov → ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)))
118, 10mpcom 36 . . . . . 6 (𝐴 ∈ Markov → ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅))
1211adantr 276 . . . . 5 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅))
13 elmapi 6664 . . . . . . . . . 10 (𝑓 ∈ (2o𝑚 𝐴) → 𝑓:𝐴⟶2o)
1413adantl 277 . . . . . . . . 9 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → 𝑓:𝐴⟶2o)
1514ffvelcdmda 5647 . . . . . . . 8 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑧𝐴) → (𝑓𝑧) ∈ 2o)
16 2oconcl 6434 . . . . . . . 8 ((𝑓𝑧) ∈ 2o → (1o ∖ (𝑓𝑧)) ∈ 2o)
1715, 16syl 14 . . . . . . 7 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑧𝐴) → (1o ∖ (𝑓𝑧)) ∈ 2o)
1817fmpttd 5667 . . . . . 6 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))):𝐴⟶2o)
19 2onn 6516 . . . . . . . 8 2o ∈ ω
2019a1i 9 . . . . . . 7 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → 2o ∈ ω)
21 simpl 109 . . . . . . 7 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → 𝐴 ∈ Markov)
2220, 21elmapd 6656 . . . . . 6 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) ∈ (2o𝑚 𝐴) ↔ (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))):𝐴⟶2o))
2318, 22mpbird 167 . . . . 5 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) ∈ (2o𝑚 𝐴))
247, 12, 23rspcdva 2846 . . . 4 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (¬ ∀𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o → ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = ∅))
25 eqid 2177 . . . . . . . . . 10 (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))
26 fveq2 5511 . . . . . . . . . . 11 (𝑧 = 𝑥 → (𝑓𝑧) = (𝑓𝑥))
2726difeq2d 3253 . . . . . . . . . 10 (𝑧 = 𝑥 → (1o ∖ (𝑓𝑧)) = (1o ∖ (𝑓𝑥)))
28 simpr 110 . . . . . . . . . 10 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑥𝐴)
29 1oex 6419 . . . . . . . . . . 11 1o ∈ V
30 difexg 4141 . . . . . . . . . . 11 (1o ∈ V → (1o ∖ (𝑓𝑥)) ∈ V)
3129, 30mp1i 10 . . . . . . . . . 10 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (1o ∖ (𝑓𝑥)) ∈ V)
3225, 27, 28, 31fvmptd3 5605 . . . . . . . . 9 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = (1o ∖ (𝑓𝑥)))
3332eqeq1d 2186 . . . . . . . 8 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o ↔ (1o ∖ (𝑓𝑥)) = 1o))
34 difeq2 3247 . . . . . . . . . . . 12 ((𝑓𝑥) = ∅ → (1o ∖ (𝑓𝑥)) = (1o ∖ ∅))
35 dif0 3493 . . . . . . . . . . . 12 (1o ∖ ∅) = 1o
3634, 35eqtrdi 2226 . . . . . . . . . . 11 ((𝑓𝑥) = ∅ → (1o ∖ (𝑓𝑥)) = 1o)
3736adantl 277 . . . . . . . . . 10 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = ∅) → (1o ∖ (𝑓𝑥)) = 1o)
38 1n0 6427 . . . . . . . . . . . . 13 1o ≠ ∅
3938nesymi 2393 . . . . . . . . . . . 12 ¬ ∅ = 1o
40 eqeq1 2184 . . . . . . . . . . . 12 ((𝑓𝑥) = ∅ → ((𝑓𝑥) = 1o ↔ ∅ = 1o))
4139, 40mtbiri 675 . . . . . . . . . . 11 ((𝑓𝑥) = ∅ → ¬ (𝑓𝑥) = 1o)
4241adantl 277 . . . . . . . . . 10 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = ∅) → ¬ (𝑓𝑥) = 1o)
4337, 422thd 175 . . . . . . . . 9 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = ∅) → ((1o ∖ (𝑓𝑥)) = 1o ↔ ¬ (𝑓𝑥) = 1o))
44 difid 3491 . . . . . . . . . . . . . 14 (1o ∖ 1o) = ∅
4544eqeq1i 2185 . . . . . . . . . . . . 13 ((1o ∖ 1o) = 1o ↔ ∅ = 1o)
4639, 45mtbir 671 . . . . . . . . . . . 12 ¬ (1o ∖ 1o) = 1o
47 difeq2 3247 . . . . . . . . . . . . 13 ((𝑓𝑥) = 1o → (1o ∖ (𝑓𝑥)) = (1o ∖ 1o))
4847eqeq1d 2186 . . . . . . . . . . . 12 ((𝑓𝑥) = 1o → ((1o ∖ (𝑓𝑥)) = 1o ↔ (1o ∖ 1o) = 1o))
4946, 48mtbiri 675 . . . . . . . . . . 11 ((𝑓𝑥) = 1o → ¬ (1o ∖ (𝑓𝑥)) = 1o)
5049adantl 277 . . . . . . . . . 10 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = 1o) → ¬ (1o ∖ (𝑓𝑥)) = 1o)
51 notnot 629 . . . . . . . . . . 11 ((𝑓𝑥) = 1o → ¬ ¬ (𝑓𝑥) = 1o)
5251adantl 277 . . . . . . . . . 10 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = 1o) → ¬ ¬ (𝑓𝑥) = 1o)
5350, 522falsed 702 . . . . . . . . 9 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = 1o) → ((1o ∖ (𝑓𝑥)) = 1o ↔ ¬ (𝑓𝑥) = 1o))
5414ffvelcdmda 5647 . . . . . . . . . . 11 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ 2o)
55 df2o3 6425 . . . . . . . . . . 11 2o = {∅, 1o}
5654, 55eleqtrdi 2270 . . . . . . . . . 10 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ {∅, 1o})
57 elpri 3614 . . . . . . . . . 10 ((𝑓𝑥) ∈ {∅, 1o} → ((𝑓𝑥) = ∅ ∨ (𝑓𝑥) = 1o))
5856, 57syl 14 . . . . . . . . 9 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝑓𝑥) = ∅ ∨ (𝑓𝑥) = 1o))
5943, 53, 58mpjaodan 798 . . . . . . . 8 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((1o ∖ (𝑓𝑥)) = 1o ↔ ¬ (𝑓𝑥) = 1o))
6033, 59bitrd 188 . . . . . . 7 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o ↔ ¬ (𝑓𝑥) = 1o))
6160ralbidva 2473 . . . . . 6 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (∀𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o ↔ ∀𝑥𝐴 ¬ (𝑓𝑥) = 1o))
6261notbid 667 . . . . 5 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (¬ ∀𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o ↔ ¬ ∀𝑥𝐴 ¬ (𝑓𝑥) = 1o))
63 ralnex 2465 . . . . . 6 (∀𝑥𝐴 ¬ (𝑓𝑥) = 1o ↔ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o)
6463notbii 668 . . . . 5 (¬ ∀𝑥𝐴 ¬ (𝑓𝑥) = 1o ↔ ¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o)
6562, 64bitrdi 196 . . . 4 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (¬ ∀𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o ↔ ¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o))
6632eqeq1d 2186 . . . . . 6 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = ∅ ↔ (1o ∖ (𝑓𝑥)) = ∅))
6735eqeq1i 2185 . . . . . . . . . . 11 ((1o ∖ ∅) = ∅ ↔ 1o = ∅)
6838, 67nemtbir 2436 . . . . . . . . . 10 ¬ (1o ∖ ∅) = ∅
6934eqeq1d 2186 . . . . . . . . . 10 ((𝑓𝑥) = ∅ → ((1o ∖ (𝑓𝑥)) = ∅ ↔ (1o ∖ ∅) = ∅))
7068, 69mtbiri 675 . . . . . . . . 9 ((𝑓𝑥) = ∅ → ¬ (1o ∖ (𝑓𝑥)) = ∅)
7170adantl 277 . . . . . . . 8 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = ∅) → ¬ (1o ∖ (𝑓𝑥)) = ∅)
7271, 422falsed 702 . . . . . . 7 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = ∅) → ((1o ∖ (𝑓𝑥)) = ∅ ↔ (𝑓𝑥) = 1o))
7347, 44eqtrdi 2226 . . . . . . . . 9 ((𝑓𝑥) = 1o → (1o ∖ (𝑓𝑥)) = ∅)
7473adantl 277 . . . . . . . 8 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = 1o) → (1o ∖ (𝑓𝑥)) = ∅)
75 simpr 110 . . . . . . . 8 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = 1o) → (𝑓𝑥) = 1o)
7674, 752thd 175 . . . . . . 7 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = 1o) → ((1o ∖ (𝑓𝑥)) = ∅ ↔ (𝑓𝑥) = 1o))
7772, 76, 58mpjaodan 798 . . . . . 6 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((1o ∖ (𝑓𝑥)) = ∅ ↔ (𝑓𝑥) = 1o))
7866, 77bitrd 188 . . . . 5 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = ∅ ↔ (𝑓𝑥) = 1o))
7978rexbidva 2474 . . . 4 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = ∅ ↔ ∃𝑥𝐴 (𝑓𝑥) = 1o))
8024, 65, 793imtr3d 202 . . 3 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o))
8180ralrimiva 2550 . 2 (𝐴 ∈ Markov → ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o))
82 elex 2748 . . . . 5 (𝐴𝑉𝐴 ∈ V)
8382adantr 276 . . . 4 ((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) → 𝐴 ∈ V)
84 fveq1 5510 . . . . . . . . . . . 12 (𝑓 = (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) → (𝑓𝑥) = ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥))
8584eqeq1d 2186 . . . . . . . . . . 11 (𝑓 = (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) → ((𝑓𝑥) = 1o ↔ ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o))
8685rexbidv 2478 . . . . . . . . . 10 (𝑓 = (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) → (∃𝑥𝐴 (𝑓𝑥) = 1o ↔ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o))
8786notbid 667 . . . . . . . . 9 (𝑓 = (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) → (¬ ∃𝑥𝐴 (𝑓𝑥) = 1o ↔ ¬ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o))
8887notbid 667 . . . . . . . 8 (𝑓 = (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) → (¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o ↔ ¬ ¬ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o))
8988, 86imbi12d 234 . . . . . . 7 (𝑓 = (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) → ((¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o) ↔ (¬ ¬ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o → ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o)))
90 simplr 528 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o))
91 elmapi 6664 . . . . . . . . . . . 12 (𝑔 ∈ (2o𝑚 𝐴) → 𝑔:𝐴⟶2o)
9291adantl 277 . . . . . . . . . . 11 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → 𝑔:𝐴⟶2o)
9392ffvelcdmda 5647 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑧𝐴) → (𝑔𝑧) ∈ 2o)
94 2oconcl 6434 . . . . . . . . . 10 ((𝑔𝑧) ∈ 2o → (1o ∖ (𝑔𝑧)) ∈ 2o)
9593, 94syl 14 . . . . . . . . 9 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑧𝐴) → (1o ∖ (𝑔𝑧)) ∈ 2o)
9695fmpttd 5667 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))):𝐴⟶2o)
9719a1i 9 . . . . . . . . 9 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → 2o ∈ ω)
98 simpll 527 . . . . . . . . 9 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → 𝐴𝑉)
9997, 98elmapd 6656 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) ∈ (2o𝑚 𝐴) ↔ (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))):𝐴⟶2o))
10096, 99mpbird 167 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) ∈ (2o𝑚 𝐴))
10189, 90, 100rspcdva 2846 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (¬ ¬ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o → ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o))
102 ralnex 2465 . . . . . . . 8 (∀𝑥𝐴 ¬ ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ ¬ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o)
103102notbii 668 . . . . . . 7 (¬ ∀𝑥𝐴 ¬ ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ ¬ ¬ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o)
104 nfv 1528 . . . . . . . . . . 11 𝑥 𝐴𝑉
105 nfcv 2319 . . . . . . . . . . . 12 𝑥(2o𝑚 𝐴)
106 nfre1 2520 . . . . . . . . . . . . . . 15 𝑥𝑥𝐴 (𝑓𝑥) = 1o
107106nfn 1658 . . . . . . . . . . . . . 14 𝑥 ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o
108107nfn 1658 . . . . . . . . . . . . 13 𝑥 ¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o
109108, 106nfim 1572 . . . . . . . . . . . 12 𝑥(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)
110105, 109nfralxy 2515 . . . . . . . . . . 11 𝑥𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)
111104, 110nfan 1565 . . . . . . . . . 10 𝑥(𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o))
112 nfv 1528 . . . . . . . . . 10 𝑥 𝑔 ∈ (2o𝑚 𝐴)
113111, 112nfan 1565 . . . . . . . . 9 𝑥((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴))
114 eqid 2177 . . . . . . . . . . . . 13 (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) = (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))
115 fveq2 5511 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (𝑔𝑧) = (𝑔𝑥))
116115difeq2d 3253 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (1o ∖ (𝑔𝑧)) = (1o ∖ (𝑔𝑥)))
117 simpr 110 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑥𝐴)
118 difexg 4141 . . . . . . . . . . . . . 14 (1o ∈ V → (1o ∖ (𝑔𝑥)) ∈ V)
11929, 118mp1i 10 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (1o ∖ (𝑔𝑥)) ∈ V)
120114, 116, 117, 119fvmptd3 5605 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = (1o ∖ (𝑔𝑥)))
121120eqeq1d 2186 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ (1o ∖ (𝑔𝑥)) = 1o))
122121notbid 667 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (¬ ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ ¬ (1o ∖ (𝑔𝑥)) = 1o))
123 difeq2 3247 . . . . . . . . . . . . . . 15 ((𝑔𝑥) = ∅ → (1o ∖ (𝑔𝑥)) = (1o ∖ ∅))
124123, 35eqtrdi 2226 . . . . . . . . . . . . . 14 ((𝑔𝑥) = ∅ → (1o ∖ (𝑔𝑥)) = 1o)
125124adantl 277 . . . . . . . . . . . . 13 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = ∅) → (1o ∖ (𝑔𝑥)) = 1o)
126125notnotd 630 . . . . . . . . . . . 12 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = ∅) → ¬ ¬ (1o ∖ (𝑔𝑥)) = 1o)
127 eqeq1 2184 . . . . . . . . . . . . . 14 ((𝑔𝑥) = ∅ → ((𝑔𝑥) = 1o ↔ ∅ = 1o))
12839, 127mtbiri 675 . . . . . . . . . . . . 13 ((𝑔𝑥) = ∅ → ¬ (𝑔𝑥) = 1o)
129128adantl 277 . . . . . . . . . . . 12 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = ∅) → ¬ (𝑔𝑥) = 1o)
130126, 1292falsed 702 . . . . . . . . . . 11 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = ∅) → (¬ (1o ∖ (𝑔𝑥)) = 1o ↔ (𝑔𝑥) = 1o))
131 difeq2 3247 . . . . . . . . . . . . . . 15 ((𝑔𝑥) = 1o → (1o ∖ (𝑔𝑥)) = (1o ∖ 1o))
132131eqeq1d 2186 . . . . . . . . . . . . . 14 ((𝑔𝑥) = 1o → ((1o ∖ (𝑔𝑥)) = 1o ↔ (1o ∖ 1o) = 1o))
13346, 132mtbiri 675 . . . . . . . . . . . . 13 ((𝑔𝑥) = 1o → ¬ (1o ∖ (𝑔𝑥)) = 1o)
134133adantl 277 . . . . . . . . . . . 12 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = 1o) → ¬ (1o ∖ (𝑔𝑥)) = 1o)
135 simpr 110 . . . . . . . . . . . 12 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = 1o) → (𝑔𝑥) = 1o)
136134, 1352thd 175 . . . . . . . . . . 11 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = 1o) → (¬ (1o ∖ (𝑔𝑥)) = 1o ↔ (𝑔𝑥) = 1o))
13791ad2antlr 489 . . . . . . . . . . . . . 14 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑔:𝐴⟶2o)
138137, 117ffvelcdmd 5648 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑔𝑥) ∈ 2o)
139138, 55eleqtrdi 2270 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑔𝑥) ∈ {∅, 1o})
140 elpri 3614 . . . . . . . . . . . 12 ((𝑔𝑥) ∈ {∅, 1o} → ((𝑔𝑥) = ∅ ∨ (𝑔𝑥) = 1o))
141139, 140syl 14 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝑔𝑥) = ∅ ∨ (𝑔𝑥) = 1o))
142130, 136, 141mpjaodan 798 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (¬ (1o ∖ (𝑔𝑥)) = 1o ↔ (𝑔𝑥) = 1o))
143122, 142bitrd 188 . . . . . . . . 9 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (¬ ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ (𝑔𝑥) = 1o))
144113, 143ralbida 2471 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∀𝑥𝐴 ¬ ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ ∀𝑥𝐴 (𝑔𝑥) = 1o))
145144notbid 667 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (¬ ∀𝑥𝐴 ¬ ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ ¬ ∀𝑥𝐴 (𝑔𝑥) = 1o))
146103, 145bitr3id 194 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (¬ ¬ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ ¬ ∀𝑥𝐴 (𝑔𝑥) = 1o))
147 simpr 110 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = ∅) → (𝑔𝑥) = ∅)
148125, 1472thd 175 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = ∅) → ((1o ∖ (𝑔𝑥)) = 1o ↔ (𝑔𝑥) = ∅))
149128, 135nsyl3 626 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = 1o) → ¬ (𝑔𝑥) = ∅)
150134, 1492falsed 702 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = 1o) → ((1o ∖ (𝑔𝑥)) = 1o ↔ (𝑔𝑥) = ∅))
151148, 150, 141mpjaodan 798 . . . . . . . 8 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((1o ∖ (𝑔𝑥)) = 1o ↔ (𝑔𝑥) = ∅))
152121, 151bitrd 188 . . . . . . 7 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ (𝑔𝑥) = ∅))
153113, 152rexbida 2472 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ ∃𝑥𝐴 (𝑔𝑥) = ∅))
154101, 146, 1533imtr3d 202 . . . . 5 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅))
155154ralrimiva 2550 . . . 4 ((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) → ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅))
1569biimprd 158 . . . 4 (𝐴 ∈ V → (∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅) → 𝐴 ∈ Markov))
15783, 155, 156sylc 62 . . 3 ((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) → 𝐴 ∈ Markov)
158157ex 115 . 2 (𝐴𝑉 → (∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o) → 𝐴 ∈ Markov))
15981, 158impbid2 143 1 (𝐴𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708   = wceq 1353  wcel 2148  wral 2455  wrex 2456  Vcvv 2737  cdif 3126  c0 3422  {cpr 3592  cmpt 4061  ωcom 4586  wf 5208  cfv 5212  (class class class)co 5869  1oc1o 6404  2oc2o 6405  𝑚 cmap 6642  Markovcmarkov 7143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-iord 4363  df-on 4365  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1o 6411  df-2o 6412  df-map 6644  df-markov 7144
This theorem is referenced by:  subctctexmid  14406
  Copyright terms: Public domain W3C validator