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

Theorem ismkvnex 7077
 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 5460 . . . . . . . . 9 (𝑔 = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) → (𝑔𝑥) = ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥))
21eqeq1d 2163 . . . . . . . 8 (𝑔 = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) → ((𝑔𝑥) = 1o ↔ ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o))
32ralbidv 2454 . . . . . . 7 (𝑔 = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) → (∀𝑥𝐴 (𝑔𝑥) = 1o ↔ ∀𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o))
43notbid 657 . . . . . 6 (𝑔 = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) → (¬ ∀𝑥𝐴 (𝑔𝑥) = 1o ↔ ¬ ∀𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o))
51eqeq1d 2163 . . . . . . 7 (𝑔 = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) → ((𝑔𝑥) = ∅ ↔ ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = ∅))
65rexbidv 2455 . . . . . 6 (𝑔 = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) → (∃𝑥𝐴 (𝑔𝑥) = ∅ ↔ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = ∅))
74, 6imbi12d 233 . . . . 5 (𝑔 = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) → ((¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅) ↔ (¬ ∀𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o → ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = ∅)))
8 elex 2720 . . . . . . 7 (𝐴 ∈ Markov → 𝐴 ∈ V)
9 ismkvmap 7076 . . . . . . . 8 (𝐴 ∈ V → (𝐴 ∈ Markov ↔ ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)))
109biimpd 143 . . . . . . 7 (𝐴 ∈ V → (𝐴 ∈ Markov → ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅)))
118, 10mpcom 36 . . . . . 6 (𝐴 ∈ Markov → ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅))
1211adantr 274 . . . . 5 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅))
13 elmapi 6604 . . . . . . . . . 10 (𝑓 ∈ (2o𝑚 𝐴) → 𝑓:𝐴⟶2o)
1413adantl 275 . . . . . . . . 9 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → 𝑓:𝐴⟶2o)
1514ffvelrnda 5595 . . . . . . . 8 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑧𝐴) → (𝑓𝑧) ∈ 2o)
16 2oconcl 6376 . . . . . . . 8 ((𝑓𝑧) ∈ 2o → (1o ∖ (𝑓𝑧)) ∈ 2o)
1715, 16syl 14 . . . . . . 7 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑧𝐴) → (1o ∖ (𝑓𝑧)) ∈ 2o)
1817fmpttd 5615 . . . . . 6 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))):𝐴⟶2o)
19 2onn 6457 . . . . . . . 8 2o ∈ ω
2019a1i 9 . . . . . . 7 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → 2o ∈ ω)
21 simpl 108 . . . . . . 7 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → 𝐴 ∈ Markov)
2220, 21elmapd 6596 . . . . . 6 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) ∈ (2o𝑚 𝐴) ↔ (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))):𝐴⟶2o))
2318, 22mpbird 166 . . . . 5 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) ∈ (2o𝑚 𝐴))
247, 12, 23rspcdva 2818 . . . 4 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (¬ ∀𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o → ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = ∅))
25 eqid 2154 . . . . . . . . . 10 (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧))) = (𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))
26 fveq2 5461 . . . . . . . . . . 11 (𝑧 = 𝑥 → (𝑓𝑧) = (𝑓𝑥))
2726difeq2d 3221 . . . . . . . . . 10 (𝑧 = 𝑥 → (1o ∖ (𝑓𝑧)) = (1o ∖ (𝑓𝑥)))
28 simpr 109 . . . . . . . . . 10 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑥𝐴)
29 1oex 6361 . . . . . . . . . . 11 1o ∈ V
30 difexg 4101 . . . . . . . . . . 11 (1o ∈ V → (1o ∖ (𝑓𝑥)) ∈ V)
3129, 30mp1i 10 . . . . . . . . . 10 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (1o ∖ (𝑓𝑥)) ∈ V)
3225, 27, 28, 31fvmptd3 5554 . . . . . . . . 9 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = (1o ∖ (𝑓𝑥)))
3332eqeq1d 2163 . . . . . . . 8 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o ↔ (1o ∖ (𝑓𝑥)) = 1o))
34 difeq2 3215 . . . . . . . . . . . 12 ((𝑓𝑥) = ∅ → (1o ∖ (𝑓𝑥)) = (1o ∖ ∅))
35 dif0 3460 . . . . . . . . . . . 12 (1o ∖ ∅) = 1o
3634, 35eqtrdi 2203 . . . . . . . . . . 11 ((𝑓𝑥) = ∅ → (1o ∖ (𝑓𝑥)) = 1o)
3736adantl 275 . . . . . . . . . 10 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = ∅) → (1o ∖ (𝑓𝑥)) = 1o)
38 1n0 6369 . . . . . . . . . . . . 13 1o ≠ ∅
3938nesymi 2370 . . . . . . . . . . . 12 ¬ ∅ = 1o
40 eqeq1 2161 . . . . . . . . . . . 12 ((𝑓𝑥) = ∅ → ((𝑓𝑥) = 1o ↔ ∅ = 1o))
4139, 40mtbiri 665 . . . . . . . . . . 11 ((𝑓𝑥) = ∅ → ¬ (𝑓𝑥) = 1o)
4241adantl 275 . . . . . . . . . 10 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = ∅) → ¬ (𝑓𝑥) = 1o)
4337, 422thd 174 . . . . . . . . 9 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = ∅) → ((1o ∖ (𝑓𝑥)) = 1o ↔ ¬ (𝑓𝑥) = 1o))
44 difid 3458 . . . . . . . . . . . . . 14 (1o ∖ 1o) = ∅
4544eqeq1i 2162 . . . . . . . . . . . . 13 ((1o ∖ 1o) = 1o ↔ ∅ = 1o)
4639, 45mtbir 661 . . . . . . . . . . . 12 ¬ (1o ∖ 1o) = 1o
47 difeq2 3215 . . . . . . . . . . . . 13 ((𝑓𝑥) = 1o → (1o ∖ (𝑓𝑥)) = (1o ∖ 1o))
4847eqeq1d 2163 . . . . . . . . . . . 12 ((𝑓𝑥) = 1o → ((1o ∖ (𝑓𝑥)) = 1o ↔ (1o ∖ 1o) = 1o))
4946, 48mtbiri 665 . . . . . . . . . . 11 ((𝑓𝑥) = 1o → ¬ (1o ∖ (𝑓𝑥)) = 1o)
5049adantl 275 . . . . . . . . . 10 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = 1o) → ¬ (1o ∖ (𝑓𝑥)) = 1o)
51 notnot 619 . . . . . . . . . . 11 ((𝑓𝑥) = 1o → ¬ ¬ (𝑓𝑥) = 1o)
5251adantl 275 . . . . . . . . . 10 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = 1o) → ¬ ¬ (𝑓𝑥) = 1o)
5350, 522falsed 692 . . . . . . . . 9 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = 1o) → ((1o ∖ (𝑓𝑥)) = 1o ↔ ¬ (𝑓𝑥) = 1o))
5414ffvelrnda 5595 . . . . . . . . . . 11 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ 2o)
55 df2o3 6367 . . . . . . . . . . 11 2o = {∅, 1o}
5654, 55eleqtrdi 2247 . . . . . . . . . 10 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ {∅, 1o})
57 elpri 3579 . . . . . . . . . 10 ((𝑓𝑥) ∈ {∅, 1o} → ((𝑓𝑥) = ∅ ∨ (𝑓𝑥) = 1o))
5856, 57syl 14 . . . . . . . . 9 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝑓𝑥) = ∅ ∨ (𝑓𝑥) = 1o))
5943, 53, 58mpjaodan 788 . . . . . . . 8 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((1o ∖ (𝑓𝑥)) = 1o ↔ ¬ (𝑓𝑥) = 1o))
6033, 59bitrd 187 . . . . . . 7 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o ↔ ¬ (𝑓𝑥) = 1o))
6160ralbidva 2450 . . . . . 6 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (∀𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o ↔ ∀𝑥𝐴 ¬ (𝑓𝑥) = 1o))
6261notbid 657 . . . . 5 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (¬ ∀𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o ↔ ¬ ∀𝑥𝐴 ¬ (𝑓𝑥) = 1o))
63 ralnex 2442 . . . . . 6 (∀𝑥𝐴 ¬ (𝑓𝑥) = 1o ↔ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o)
6463notbii 658 . . . . 5 (¬ ∀𝑥𝐴 ¬ (𝑓𝑥) = 1o ↔ ¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o)
6562, 64bitrdi 195 . . . 4 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (¬ ∀𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = 1o ↔ ¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o))
6632eqeq1d 2163 . . . . . 6 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = ∅ ↔ (1o ∖ (𝑓𝑥)) = ∅))
6735eqeq1i 2162 . . . . . . . . . . 11 ((1o ∖ ∅) = ∅ ↔ 1o = ∅)
6838, 67nemtbir 2413 . . . . . . . . . 10 ¬ (1o ∖ ∅) = ∅
6934eqeq1d 2163 . . . . . . . . . 10 ((𝑓𝑥) = ∅ → ((1o ∖ (𝑓𝑥)) = ∅ ↔ (1o ∖ ∅) = ∅))
7068, 69mtbiri 665 . . . . . . . . 9 ((𝑓𝑥) = ∅ → ¬ (1o ∖ (𝑓𝑥)) = ∅)
7170adantl 275 . . . . . . . 8 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = ∅) → ¬ (1o ∖ (𝑓𝑥)) = ∅)
7271, 422falsed 692 . . . . . . 7 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = ∅) → ((1o ∖ (𝑓𝑥)) = ∅ ↔ (𝑓𝑥) = 1o))
7347, 44eqtrdi 2203 . . . . . . . . 9 ((𝑓𝑥) = 1o → (1o ∖ (𝑓𝑥)) = ∅)
7473adantl 275 . . . . . . . 8 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = 1o) → (1o ∖ (𝑓𝑥)) = ∅)
75 simpr 109 . . . . . . . 8 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = 1o) → (𝑓𝑥) = 1o)
7674, 752thd 174 . . . . . . 7 ((((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑓𝑥) = 1o) → ((1o ∖ (𝑓𝑥)) = ∅ ↔ (𝑓𝑥) = 1o))
7772, 76, 58mpjaodan 788 . . . . . 6 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((1o ∖ (𝑓𝑥)) = ∅ ↔ (𝑓𝑥) = 1o))
7866, 77bitrd 187 . . . . 5 (((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = ∅ ↔ (𝑓𝑥) = 1o))
7978rexbidva 2451 . . . 4 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑓𝑧)))‘𝑥) = ∅ ↔ ∃𝑥𝐴 (𝑓𝑥) = 1o))
8024, 65, 793imtr3d 201 . . 3 ((𝐴 ∈ Markov ∧ 𝑓 ∈ (2o𝑚 𝐴)) → (¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o))
8180ralrimiva 2527 . 2 (𝐴 ∈ Markov → ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o))
82 elex 2720 . . . . 5 (𝐴𝑉𝐴 ∈ V)
8382adantr 274 . . . 4 ((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) → 𝐴 ∈ V)
84 fveq1 5460 . . . . . . . . . . . 12 (𝑓 = (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) → (𝑓𝑥) = ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥))
8584eqeq1d 2163 . . . . . . . . . . 11 (𝑓 = (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) → ((𝑓𝑥) = 1o ↔ ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o))
8685rexbidv 2455 . . . . . . . . . 10 (𝑓 = (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) → (∃𝑥𝐴 (𝑓𝑥) = 1o ↔ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o))
8786notbid 657 . . . . . . . . 9 (𝑓 = (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) → (¬ ∃𝑥𝐴 (𝑓𝑥) = 1o ↔ ¬ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o))
8887notbid 657 . . . . . . . 8 (𝑓 = (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) → (¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o ↔ ¬ ¬ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o))
8988, 86imbi12d 233 . . . . . . 7 (𝑓 = (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) → ((¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o) ↔ (¬ ¬ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o → ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o)))
90 simplr 520 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o))
91 elmapi 6604 . . . . . . . . . . . 12 (𝑔 ∈ (2o𝑚 𝐴) → 𝑔:𝐴⟶2o)
9291adantl 275 . . . . . . . . . . 11 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → 𝑔:𝐴⟶2o)
9392ffvelrnda 5595 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑧𝐴) → (𝑔𝑧) ∈ 2o)
94 2oconcl 6376 . . . . . . . . . 10 ((𝑔𝑧) ∈ 2o → (1o ∖ (𝑔𝑧)) ∈ 2o)
9593, 94syl 14 . . . . . . . . 9 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑧𝐴) → (1o ∖ (𝑔𝑧)) ∈ 2o)
9695fmpttd 5615 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))):𝐴⟶2o)
9719a1i 9 . . . . . . . . 9 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → 2o ∈ ω)
98 simpll 519 . . . . . . . . 9 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → 𝐴𝑉)
9997, 98elmapd 6596 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) ∈ (2o𝑚 𝐴) ↔ (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))):𝐴⟶2o))
10096, 99mpbird 166 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) ∈ (2o𝑚 𝐴))
10189, 90, 100rspcdva 2818 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (¬ ¬ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o → ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o))
102 ralnex 2442 . . . . . . . 8 (∀𝑥𝐴 ¬ ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ ¬ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o)
103102notbii 658 . . . . . . 7 (¬ ∀𝑥𝐴 ¬ ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ ¬ ¬ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o)
104 nfv 1505 . . . . . . . . . . 11 𝑥 𝐴𝑉
105 nfcv 2296 . . . . . . . . . . . 12 𝑥(2o𝑚 𝐴)
106 nfre1 2497 . . . . . . . . . . . . . . 15 𝑥𝑥𝐴 (𝑓𝑥) = 1o
107106nfn 1635 . . . . . . . . . . . . . 14 𝑥 ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o
108107nfn 1635 . . . . . . . . . . . . 13 𝑥 ¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o
109108, 106nfim 1549 . . . . . . . . . . . 12 𝑥(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)
110105, 109nfralxy 2492 . . . . . . . . . . 11 𝑥𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)
111104, 110nfan 1542 . . . . . . . . . 10 𝑥(𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o))
112 nfv 1505 . . . . . . . . . 10 𝑥 𝑔 ∈ (2o𝑚 𝐴)
113111, 112nfan 1542 . . . . . . . . 9 𝑥((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴))
114 eqid 2154 . . . . . . . . . . . . 13 (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧))) = (𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))
115 fveq2 5461 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (𝑔𝑧) = (𝑔𝑥))
116115difeq2d 3221 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (1o ∖ (𝑔𝑧)) = (1o ∖ (𝑔𝑥)))
117 simpr 109 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑥𝐴)
118 difexg 4101 . . . . . . . . . . . . . 14 (1o ∈ V → (1o ∖ (𝑔𝑥)) ∈ V)
11929, 118mp1i 10 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (1o ∖ (𝑔𝑥)) ∈ V)
120114, 116, 117, 119fvmptd3 5554 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = (1o ∖ (𝑔𝑥)))
121120eqeq1d 2163 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ (1o ∖ (𝑔𝑥)) = 1o))
122121notbid 657 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (¬ ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ ¬ (1o ∖ (𝑔𝑥)) = 1o))
123 difeq2 3215 . . . . . . . . . . . . . . 15 ((𝑔𝑥) = ∅ → (1o ∖ (𝑔𝑥)) = (1o ∖ ∅))
124123, 35eqtrdi 2203 . . . . . . . . . . . . . 14 ((𝑔𝑥) = ∅ → (1o ∖ (𝑔𝑥)) = 1o)
125124adantl 275 . . . . . . . . . . . . 13 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = ∅) → (1o ∖ (𝑔𝑥)) = 1o)
126125notnotd 620 . . . . . . . . . . . 12 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = ∅) → ¬ ¬ (1o ∖ (𝑔𝑥)) = 1o)
127 eqeq1 2161 . . . . . . . . . . . . . 14 ((𝑔𝑥) = ∅ → ((𝑔𝑥) = 1o ↔ ∅ = 1o))
12839, 127mtbiri 665 . . . . . . . . . . . . 13 ((𝑔𝑥) = ∅ → ¬ (𝑔𝑥) = 1o)
129128adantl 275 . . . . . . . . . . . 12 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = ∅) → ¬ (𝑔𝑥) = 1o)
130126, 1292falsed 692 . . . . . . . . . . 11 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = ∅) → (¬ (1o ∖ (𝑔𝑥)) = 1o ↔ (𝑔𝑥) = 1o))
131 difeq2 3215 . . . . . . . . . . . . . . 15 ((𝑔𝑥) = 1o → (1o ∖ (𝑔𝑥)) = (1o ∖ 1o))
132131eqeq1d 2163 . . . . . . . . . . . . . 14 ((𝑔𝑥) = 1o → ((1o ∖ (𝑔𝑥)) = 1o ↔ (1o ∖ 1o) = 1o))
13346, 132mtbiri 665 . . . . . . . . . . . . 13 ((𝑔𝑥) = 1o → ¬ (1o ∖ (𝑔𝑥)) = 1o)
134133adantl 275 . . . . . . . . . . . 12 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = 1o) → ¬ (1o ∖ (𝑔𝑥)) = 1o)
135 simpr 109 . . . . . . . . . . . 12 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = 1o) → (𝑔𝑥) = 1o)
136134, 1352thd 174 . . . . . . . . . . 11 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = 1o) → (¬ (1o ∖ (𝑔𝑥)) = 1o ↔ (𝑔𝑥) = 1o))
13791ad2antlr 481 . . . . . . . . . . . . . 14 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑔:𝐴⟶2o)
138137, 117ffvelrnd 5596 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑔𝑥) ∈ 2o)
139138, 55eleqtrdi 2247 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑔𝑥) ∈ {∅, 1o})
140 elpri 3579 . . . . . . . . . . . 12 ((𝑔𝑥) ∈ {∅, 1o} → ((𝑔𝑥) = ∅ ∨ (𝑔𝑥) = 1o))
141139, 140syl 14 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝑔𝑥) = ∅ ∨ (𝑔𝑥) = 1o))
142130, 136, 141mpjaodan 788 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (¬ (1o ∖ (𝑔𝑥)) = 1o ↔ (𝑔𝑥) = 1o))
143122, 142bitrd 187 . . . . . . . . 9 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (¬ ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ (𝑔𝑥) = 1o))
144113, 143ralbida 2448 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∀𝑥𝐴 ¬ ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ ∀𝑥𝐴 (𝑔𝑥) = 1o))
145144notbid 657 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (¬ ∀𝑥𝐴 ¬ ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ ¬ ∀𝑥𝐴 (𝑔𝑥) = 1o))
146103, 145bitr3id 193 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (¬ ¬ ∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ ¬ ∀𝑥𝐴 (𝑔𝑥) = 1o))
147 simpr 109 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = ∅) → (𝑔𝑥) = ∅)
148125, 1472thd 174 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = ∅) → ((1o ∖ (𝑔𝑥)) = 1o ↔ (𝑔𝑥) = ∅))
149128, 135nsyl3 616 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = 1o) → ¬ (𝑔𝑥) = ∅)
150134, 1492falsed 692 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ (𝑔𝑥) = 1o) → ((1o ∖ (𝑔𝑥)) = 1o ↔ (𝑔𝑥) = ∅))
151148, 150, 141mpjaodan 788 . . . . . . . 8 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((1o ∖ (𝑔𝑥)) = 1o ↔ (𝑔𝑥) = ∅))
152121, 151bitrd 187 . . . . . . 7 ((((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ (𝑔𝑥) = ∅))
153113, 152rexbida 2449 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∃𝑥𝐴 ((𝑧𝐴 ↦ (1o ∖ (𝑔𝑧)))‘𝑥) = 1o ↔ ∃𝑥𝐴 (𝑔𝑥) = ∅))
154101, 146, 1533imtr3d 201 . . . . 5 (((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅))
155154ralrimiva 2527 . . . 4 ((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) → ∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅))
1569biimprd 157 . . . 4 (𝐴 ∈ V → (∀𝑔 ∈ (2o𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑔𝑥) = 1o → ∃𝑥𝐴 (𝑔𝑥) = ∅) → 𝐴 ∈ Markov))
15783, 155, 156sylc 62 . . 3 ((𝐴𝑉 ∧ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)) → 𝐴 ∈ Markov)
158157ex 114 . 2 (𝐴𝑉 → (∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o) → 𝐴 ∈ Markov))
15981, 158impbid2 142 1 (𝐴𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ (2o𝑚 𝐴)(¬ ¬ ∃𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = 1o)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   = wceq 1332   ∈ wcel 2125  ∀wral 2432  ∃wrex 2433  Vcvv 2709   ∖ cdif 3095  ∅c0 3390  {cpr 3557   ↦ cmpt 4021  ωcom 4543  ⟶wf 5159  ‘cfv 5163  (class class class)co 5814  1oc1o 6346  2oc2o 6347   ↑𝑚 cmap 6582  Markovcmarkov 7073 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 2127  ax-14 2128  ax-ext 2136  ax-sep 4078  ax-nul 4086  ax-pow 4130  ax-pr 4164  ax-un 4388  ax-setind 4490 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ne 2325  df-ral 2437  df-rex 2438  df-rab 2441  df-v 2711  df-sbc 2934  df-csb 3028  df-dif 3100  df-un 3102  df-in 3104  df-ss 3111  df-nul 3391  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-int 3804  df-br 3962  df-opab 4022  df-mpt 4023  df-tr 4059  df-id 4248  df-iord 4321  df-on 4323  df-suc 4326  df-iom 4544  df-xp 4585  df-rel 4586  df-cnv 4587  df-co 4588  df-dm 4589  df-rn 4590  df-res 4591  df-ima 4592  df-iota 5128  df-fun 5165  df-fn 5166  df-f 5167  df-fv 5171  df-ov 5817  df-oprab 5818  df-mpo 5819  df-1o 6353  df-2o 6354  df-map 6584  df-markov 7074 This theorem is referenced by:  subctctexmid  13512
 Copyright terms: Public domain W3C validator