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

Theorem isomninnlem 13286
 Description: Lemma for isomninn 13287. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.)
Hypothesis
Ref Expression
isomninnlem.g 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
Assertion
Ref Expression
isomninnlem (𝐴𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)))
Distinct variable groups:   𝐴,𝑓,𝑥   𝑓,𝐺,𝑥   𝑓,𝑉,𝑥

Proof of Theorem isomninnlem
Dummy variables 𝑔 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isomnimap 7009 . 2 (𝐴𝑉 → (𝐴 ∈ Omni ↔ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)))
2 fveq1 5420 . . . . . . . . 9 (𝑔 = (𝐺𝑓) → (𝑔𝑥) = ((𝐺𝑓)‘𝑥))
32eqeq1d 2148 . . . . . . . 8 (𝑔 = (𝐺𝑓) → ((𝑔𝑥) = ∅ ↔ ((𝐺𝑓)‘𝑥) = ∅))
43rexbidv 2438 . . . . . . 7 (𝑔 = (𝐺𝑓) → (∃𝑥𝐴 (𝑔𝑥) = ∅ ↔ ∃𝑥𝐴 ((𝐺𝑓)‘𝑥) = ∅))
52eqeq1d 2148 . . . . . . . 8 (𝑔 = (𝐺𝑓) → ((𝑔𝑥) = 1o ↔ ((𝐺𝑓)‘𝑥) = 1o))
65ralbidv 2437 . . . . . . 7 (𝑔 = (𝐺𝑓) → (∀𝑥𝐴 (𝑔𝑥) = 1o ↔ ∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o))
74, 6orbi12d 782 . . . . . 6 (𝑔 = (𝐺𝑓) → ((∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o) ↔ (∃𝑥𝐴 ((𝐺𝑓)‘𝑥) = ∅ ∨ ∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o)))
8 simplr 519 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o))
9 isomninnlem.g . . . . . . . . . . . . 13 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
109frechashgf1o 10213 . . . . . . . . . . . 12 𝐺:ω–1-1-onto→ℕ0
11 f1ocnv 5380 . . . . . . . . . . . 12 (𝐺:ω–1-1-onto→ℕ0𝐺:ℕ01-1-onto→ω)
12 f1of 5367 . . . . . . . . . . . 12 (𝐺:ℕ01-1-onto→ω → 𝐺:ℕ0⟶ω)
1310, 11, 12mp2b 8 . . . . . . . . . . 11 𝐺:ℕ0⟶ω
14 0nn0 9004 . . . . . . . . . . . 12 0 ∈ ℕ0
15 1nn0 9005 . . . . . . . . . . . 12 1 ∈ ℕ0
16 prssi 3678 . . . . . . . . . . . 12 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
1714, 15, 16mp2an 422 . . . . . . . . . . 11 {0, 1} ⊆ ℕ0
18 fssres 5298 . . . . . . . . . . 11 ((𝐺:ℕ0⟶ω ∧ {0, 1} ⊆ ℕ0) → (𝐺 ↾ {0, 1}):{0, 1}⟶ω)
1913, 17, 18mp2an 422 . . . . . . . . . 10 (𝐺 ↾ {0, 1}):{0, 1}⟶ω
20 ffn 5272 . . . . . . . . . 10 ((𝐺 ↾ {0, 1}):{0, 1}⟶ω → (𝐺 ↾ {0, 1}) Fn {0, 1})
2119, 20ax-mp 5 . . . . . . . . 9 (𝐺 ↾ {0, 1}) Fn {0, 1}
22 fvres 5445 . . . . . . . . . . 11 (𝑗 ∈ {0, 1} → ((𝐺 ↾ {0, 1})‘𝑗) = (𝐺𝑗))
23 elpri 3550 . . . . . . . . . . . 12 (𝑗 ∈ {0, 1} → (𝑗 = 0 ∨ 𝑗 = 1))
24 fveq2 5421 . . . . . . . . . . . . . 14 (𝑗 = 0 → (𝐺𝑗) = (𝐺‘0))
25 0zd 9078 . . . . . . . . . . . . . . . . . 18 (⊤ → 0 ∈ ℤ)
2625, 9frec2uz0d 10184 . . . . . . . . . . . . . . . . 17 (⊤ → (𝐺‘∅) = 0)
2726mptru 1340 . . . . . . . . . . . . . . . 16 (𝐺‘∅) = 0
28 peano1 4508 . . . . . . . . . . . . . . . . 17 ∅ ∈ ω
29 f1ocnvfv 5680 . . . . . . . . . . . . . . . . 17 ((𝐺:ω–1-1-onto→ℕ0 ∧ ∅ ∈ ω) → ((𝐺‘∅) = 0 → (𝐺‘0) = ∅))
3010, 28, 29mp2an 422 . . . . . . . . . . . . . . . 16 ((𝐺‘∅) = 0 → (𝐺‘0) = ∅)
3127, 30ax-mp 5 . . . . . . . . . . . . . . 15 (𝐺‘0) = ∅
32 0lt2o 6338 . . . . . . . . . . . . . . 15 ∅ ∈ 2o
3331, 32eqeltri 2212 . . . . . . . . . . . . . 14 (𝐺‘0) ∈ 2o
3424, 33eqeltrdi 2230 . . . . . . . . . . . . 13 (𝑗 = 0 → (𝐺𝑗) ∈ 2o)
35 fveq2 5421 . . . . . . . . . . . . . 14 (𝑗 = 1 → (𝐺𝑗) = (𝐺‘1))
36 df-1o 6313 . . . . . . . . . . . . . . . . . 18 1o = suc ∅
3736fveq2i 5424 . . . . . . . . . . . . . . . . 17 (𝐺‘1o) = (𝐺‘suc ∅)
3828a1i 9 . . . . . . . . . . . . . . . . . . 19 (⊤ → ∅ ∈ ω)
3925, 9, 38frec2uzsucd 10186 . . . . . . . . . . . . . . . . . 18 (⊤ → (𝐺‘suc ∅) = ((𝐺‘∅) + 1))
4039mptru 1340 . . . . . . . . . . . . . . . . 17 (𝐺‘suc ∅) = ((𝐺‘∅) + 1)
4127oveq1i 5784 . . . . . . . . . . . . . . . . . 18 ((𝐺‘∅) + 1) = (0 + 1)
42 0p1e1 8846 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
4341, 42eqtri 2160 . . . . . . . . . . . . . . . . 17 ((𝐺‘∅) + 1) = 1
4437, 40, 433eqtri 2164 . . . . . . . . . . . . . . . 16 (𝐺‘1o) = 1
45 1onn 6416 . . . . . . . . . . . . . . . . 17 1o ∈ ω
46 f1ocnvfv 5680 . . . . . . . . . . . . . . . . 17 ((𝐺:ω–1-1-onto→ℕ0 ∧ 1o ∈ ω) → ((𝐺‘1o) = 1 → (𝐺‘1) = 1o))
4710, 45, 46mp2an 422 . . . . . . . . . . . . . . . 16 ((𝐺‘1o) = 1 → (𝐺‘1) = 1o)
4844, 47ax-mp 5 . . . . . . . . . . . . . . 15 (𝐺‘1) = 1o
49 1lt2o 6339 . . . . . . . . . . . . . . 15 1o ∈ 2o
5048, 49eqeltri 2212 . . . . . . . . . . . . . 14 (𝐺‘1) ∈ 2o
5135, 50eqeltrdi 2230 . . . . . . . . . . . . 13 (𝑗 = 1 → (𝐺𝑗) ∈ 2o)
5234, 51jaoi 705 . . . . . . . . . . . 12 ((𝑗 = 0 ∨ 𝑗 = 1) → (𝐺𝑗) ∈ 2o)
5323, 52syl 14 . . . . . . . . . . 11 (𝑗 ∈ {0, 1} → (𝐺𝑗) ∈ 2o)
5422, 53eqeltrd 2216 . . . . . . . . . 10 (𝑗 ∈ {0, 1} → ((𝐺 ↾ {0, 1})‘𝑗) ∈ 2o)
5554rgen 2485 . . . . . . . . 9 𝑗 ∈ {0, 1} ((𝐺 ↾ {0, 1})‘𝑗) ∈ 2o
56 ffnfv 5578 . . . . . . . . 9 ((𝐺 ↾ {0, 1}):{0, 1}⟶2o ↔ ((𝐺 ↾ {0, 1}) Fn {0, 1} ∧ ∀𝑗 ∈ {0, 1} ((𝐺 ↾ {0, 1})‘𝑗) ∈ 2o))
5721, 55, 56mpbir2an 926 . . . . . . . 8 (𝐺 ↾ {0, 1}):{0, 1}⟶2o
58 elmapi 6564 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
5958adantl 275 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝑓:𝐴⟶{0, 1})
60 fco2 5289 . . . . . . . 8 (((𝐺 ↾ {0, 1}):{0, 1}⟶2o𝑓:𝐴⟶{0, 1}) → (𝐺𝑓):𝐴⟶2o)
6157, 59, 60sylancr 410 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝐺𝑓):𝐴⟶2o)
62 2onn 6417 . . . . . . . . 9 2o ∈ ω
6362a1i 9 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 2o ∈ ω)
64 simpll 518 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝐴𝑉)
6563, 64elmapd 6556 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ((𝐺𝑓) ∈ (2o𝑚 𝐴) ↔ (𝐺𝑓):𝐴⟶2o))
6661, 65mpbird 166 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝐺𝑓) ∈ (2o𝑚 𝐴))
677, 8, 66rspcdva 2794 . . . . 5 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∃𝑥𝐴 ((𝐺𝑓)‘𝑥) = ∅ ∨ ∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o))
68 nfv 1508 . . . . . . . . 9 𝑥 𝐴𝑉
69 nfcv 2281 . . . . . . . . . 10 𝑥(2o𝑚 𝐴)
70 nfre1 2476 . . . . . . . . . . 11 𝑥𝑥𝐴 (𝑔𝑥) = ∅
71 nfra1 2466 . . . . . . . . . . 11 𝑥𝑥𝐴 (𝑔𝑥) = 1o
7270, 71nfor 1553 . . . . . . . . . 10 𝑥(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)
7369, 72nfralxy 2471 . . . . . . . . 9 𝑥𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)
7468, 73nfan 1544 . . . . . . . 8 𝑥(𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o))
75 nfv 1508 . . . . . . . 8 𝑥 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)
7674, 75nfan 1544 . . . . . . 7 𝑥((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴))
77 simplr 519 . . . . . . . . . . . . . 14 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑓 ∈ ({0, 1} ↑𝑚 𝐴))
7877, 58syl 14 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑓:𝐴⟶{0, 1})
79 simpr 109 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑥𝐴)
8078, 79ffvelrnd 5556 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ {0, 1})
8117, 80sseldi 3095 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℕ0)
82 f1ocnvfv2 5679 . . . . . . . . . . 11 ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑓𝑥) ∈ ℕ0) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝑓𝑥))
8310, 81, 82sylancr 410 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝑓𝑥))
8483adantr 274 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝑓𝑥))
85 fvco3 5492 . . . . . . . . . . . . . 14 ((𝑓:𝐴⟶{0, 1} ∧ 𝑥𝐴) → ((𝐺𝑓)‘𝑥) = (𝐺‘(𝑓𝑥)))
8678, 85sylancom 416 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝐺𝑓)‘𝑥) = (𝐺‘(𝑓𝑥)))
8786eqeq1d 2148 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑓)‘𝑥) = ∅ ↔ (𝐺‘(𝑓𝑥)) = ∅))
8887biimpa 294 . . . . . . . . . . 11 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝐺‘(𝑓𝑥)) = ∅)
8988fveq2d 5425 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝐺‘∅))
9089, 27syl6eq 2188 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝐺‘(𝐺‘(𝑓𝑥))) = 0)
9184, 90eqtr3d 2174 . . . . . . . 8 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝑓𝑥) = 0)
9291exp31 361 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝑥𝐴 → (((𝐺𝑓)‘𝑥) = ∅ → (𝑓𝑥) = 0)))
9376, 92reximdai 2530 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∃𝑥𝐴 ((𝐺𝑓)‘𝑥) = ∅ → ∃𝑥𝐴 (𝑓𝑥) = 0))
9483adantr 274 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝑓𝑥))
9586adantr 274 . . . . . . . . . . . 12 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → ((𝐺𝑓)‘𝑥) = (𝐺‘(𝑓𝑥)))
96 simpr 109 . . . . . . . . . . . 12 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → ((𝐺𝑓)‘𝑥) = 1o)
9795, 96eqtr3d 2174 . . . . . . . . . . 11 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝐺‘(𝑓𝑥)) = 1o)
9897fveq2d 5425 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝐺‘1o))
9998, 44syl6eq 2188 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝐺‘(𝐺‘(𝑓𝑥))) = 1)
10094, 99eqtr3d 2174 . . . . . . . 8 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝑓𝑥) = 1)
101100ex 114 . . . . . . 7 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑓)‘𝑥) = 1o → (𝑓𝑥) = 1))
10276, 101ralimdaa 2498 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o → ∀𝑥𝐴 (𝑓𝑥) = 1))
10393, 102orim12d 775 . . . . 5 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ((∃𝑥𝐴 ((𝐺𝑓)‘𝑥) = ∅ ∨ ∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o) → (∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)))
10467, 103mpd 13 . . . 4 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1))
105104ralrimiva 2505 . . 3 ((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1))
106 fveq1 5420 . . . . . . . . 9 (𝑓 = (𝐺𝑔) → (𝑓𝑥) = ((𝐺𝑔)‘𝑥))
107106eqeq1d 2148 . . . . . . . 8 (𝑓 = (𝐺𝑔) → ((𝑓𝑥) = 0 ↔ ((𝐺𝑔)‘𝑥) = 0))
108107rexbidv 2438 . . . . . . 7 (𝑓 = (𝐺𝑔) → (∃𝑥𝐴 (𝑓𝑥) = 0 ↔ ∃𝑥𝐴 ((𝐺𝑔)‘𝑥) = 0))
109106eqeq1d 2148 . . . . . . . 8 (𝑓 = (𝐺𝑔) → ((𝑓𝑥) = 1 ↔ ((𝐺𝑔)‘𝑥) = 1))
110109ralbidv 2437 . . . . . . 7 (𝑓 = (𝐺𝑔) → (∀𝑥𝐴 (𝑓𝑥) = 1 ↔ ∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1))
111108, 110orbi12d 782 . . . . . 6 (𝑓 = (𝐺𝑔) → ((∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1) ↔ (∃𝑥𝐴 ((𝐺𝑔)‘𝑥) = 0 ∨ ∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1)))
112 simplr 519 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1))
113 f1of 5367 . . . . . . . . . . . 12 (𝐺:ω–1-1-onto→ℕ0𝐺:ω⟶ℕ0)
11410, 113ax-mp 5 . . . . . . . . . . 11 𝐺:ω⟶ℕ0
115 omelon 4522 . . . . . . . . . . . . 13 ω ∈ On
116115onelssi 4351 . . . . . . . . . . . 12 (2o ∈ ω → 2o ⊆ ω)
11762, 116ax-mp 5 . . . . . . . . . . 11 2o ⊆ ω
118 fssres 5298 . . . . . . . . . . 11 ((𝐺:ω⟶ℕ0 ∧ 2o ⊆ ω) → (𝐺 ↾ 2o):2o⟶ℕ0)
119114, 117, 118mp2an 422 . . . . . . . . . 10 (𝐺 ↾ 2o):2o⟶ℕ0
120 ffn 5272 . . . . . . . . . 10 ((𝐺 ↾ 2o):2o⟶ℕ0 → (𝐺 ↾ 2o) Fn 2o)
121119, 120ax-mp 5 . . . . . . . . 9 (𝐺 ↾ 2o) Fn 2o
122 fvres 5445 . . . . . . . . . . 11 (𝑗 ∈ 2o → ((𝐺 ↾ 2o)‘𝑗) = (𝐺𝑗))
123 elpri 3550 . . . . . . . . . . . . 13 (𝑗 ∈ {∅, 1o} → (𝑗 = ∅ ∨ 𝑗 = 1o))
124 df2o3 6327 . . . . . . . . . . . . 13 2o = {∅, 1o}
125123, 124eleq2s 2234 . . . . . . . . . . . 12 (𝑗 ∈ 2o → (𝑗 = ∅ ∨ 𝑗 = 1o))
126 fveq2 5421 . . . . . . . . . . . . . 14 (𝑗 = ∅ → (𝐺𝑗) = (𝐺‘∅))
127 c0ex 7772 . . . . . . . . . . . . . . . 16 0 ∈ V
128127prid1 3629 . . . . . . . . . . . . . . 15 0 ∈ {0, 1}
12927, 128eqeltri 2212 . . . . . . . . . . . . . 14 (𝐺‘∅) ∈ {0, 1}
130126, 129eqeltrdi 2230 . . . . . . . . . . . . 13 (𝑗 = ∅ → (𝐺𝑗) ∈ {0, 1})
131 fveq2 5421 . . . . . . . . . . . . . 14 (𝑗 = 1o → (𝐺𝑗) = (𝐺‘1o))
132 1ex 7773 . . . . . . . . . . . . . . . 16 1 ∈ V
133132prid2 3630 . . . . . . . . . . . . . . 15 1 ∈ {0, 1}
13444, 133eqeltri 2212 . . . . . . . . . . . . . 14 (𝐺‘1o) ∈ {0, 1}
135131, 134eqeltrdi 2230 . . . . . . . . . . . . 13 (𝑗 = 1o → (𝐺𝑗) ∈ {0, 1})
136130, 135jaoi 705 . . . . . . . . . . . 12 ((𝑗 = ∅ ∨ 𝑗 = 1o) → (𝐺𝑗) ∈ {0, 1})
137125, 136syl 14 . . . . . . . . . . 11 (𝑗 ∈ 2o → (𝐺𝑗) ∈ {0, 1})
138122, 137eqeltrd 2216 . . . . . . . . . 10 (𝑗 ∈ 2o → ((𝐺 ↾ 2o)‘𝑗) ∈ {0, 1})
139138rgen 2485 . . . . . . . . 9 𝑗 ∈ 2o ((𝐺 ↾ 2o)‘𝑗) ∈ {0, 1}
140 ffnfv 5578 . . . . . . . . 9 ((𝐺 ↾ 2o):2o⟶{0, 1} ↔ ((𝐺 ↾ 2o) Fn 2o ∧ ∀𝑗 ∈ 2o ((𝐺 ↾ 2o)‘𝑗) ∈ {0, 1}))
141121, 139, 140mpbir2an 926 . . . . . . . 8 (𝐺 ↾ 2o):2o⟶{0, 1}
142 elmapi 6564 . . . . . . . . 9 (𝑔 ∈ (2o𝑚 𝐴) → 𝑔:𝐴⟶2o)
143142adantl 275 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → 𝑔:𝐴⟶2o)
144 fco2 5289 . . . . . . . 8 (((𝐺 ↾ 2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺𝑔):𝐴⟶{0, 1})
145141, 143, 144sylancr 410 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝐺𝑔):𝐴⟶{0, 1})
146 prexg 4133 . . . . . . . . . 10 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ∈ V)
14714, 15, 146mp2an 422 . . . . . . . . 9 {0, 1} ∈ V
148147a1i 9 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → {0, 1} ∈ V)
149 simpll 518 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → 𝐴𝑉)
150148, 149elmapd 6556 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → ((𝐺𝑔) ∈ ({0, 1} ↑𝑚 𝐴) ↔ (𝐺𝑔):𝐴⟶{0, 1}))
151145, 150mpbird 166 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝐺𝑔) ∈ ({0, 1} ↑𝑚 𝐴))
152111, 112, 151rspcdva 2794 . . . . 5 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∃𝑥𝐴 ((𝐺𝑔)‘𝑥) = 0 ∨ ∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1))
153 nfcv 2281 . . . . . . . . . 10 𝑥({0, 1} ↑𝑚 𝐴)
154 nfre1 2476 . . . . . . . . . . 11 𝑥𝑥𝐴 (𝑓𝑥) = 0
155 nfra1 2466 . . . . . . . . . . 11 𝑥𝑥𝐴 (𝑓𝑥) = 1
156154, 155nfor 1553 . . . . . . . . . 10 𝑥(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)
157153, 156nfralxy 2471 . . . . . . . . 9 𝑥𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)
15868, 157nfan 1544 . . . . . . . 8 𝑥(𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1))
159 nfv 1508 . . . . . . . 8 𝑥 𝑔 ∈ (2o𝑚 𝐴)
160158, 159nfan 1544 . . . . . . 7 𝑥((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴))
161143adantr 274 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑔:𝐴⟶2o)
162117a1i 9 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 2o ⊆ ω)
163161, 162fssd 5285 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑔:𝐴⟶ω)
164 simpr 109 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑥𝐴)
165163, 164ffvelrnd 5556 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑔𝑥) ∈ ω)
166 f1ocnvfv1 5678 . . . . . . . . . . 11 ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑔𝑥) ∈ ω) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝑔𝑥))
16710, 165, 166sylancr 410 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝑔𝑥))
168167adantr 274 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝑔𝑥))
169 fvco3 5492 . . . . . . . . . . . . . 14 ((𝑔:𝐴⟶2o𝑥𝐴) → ((𝐺𝑔)‘𝑥) = (𝐺‘(𝑔𝑥)))
170161, 169sylancom 416 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝐺𝑔)‘𝑥) = (𝐺‘(𝑔𝑥)))
171170eqeq1d 2148 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑔)‘𝑥) = 0 ↔ (𝐺‘(𝑔𝑥)) = 0))
172171biimpa 294 . . . . . . . . . . 11 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝐺‘(𝑔𝑥)) = 0)
173172fveq2d 5425 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝐺‘0))
174173, 31syl6eq 2188 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝐺‘(𝐺‘(𝑔𝑥))) = ∅)
175168, 174eqtr3d 2174 . . . . . . . 8 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝑔𝑥) = ∅)
176175exp31 361 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝑥𝐴 → (((𝐺𝑔)‘𝑥) = 0 → (𝑔𝑥) = ∅)))
177160, 176reximdai 2530 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∃𝑥𝐴 ((𝐺𝑔)‘𝑥) = 0 → ∃𝑥𝐴 (𝑔𝑥) = ∅))
178167adantr 274 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝑔𝑥))
179170eqeq1d 2148 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔𝑥)) = 1))
180179biimpa 294 . . . . . . . . . . 11 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝐺‘(𝑔𝑥)) = 1)
181180fveq2d 5425 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝐺‘1))
182181, 48syl6eq 2188 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝐺‘(𝐺‘(𝑔𝑥))) = 1o)
183178, 182eqtr3d 2174 . . . . . . . 8 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝑔𝑥) = 1o)
184183ex 114 . . . . . . 7 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑔)‘𝑥) = 1 → (𝑔𝑥) = 1o))
185160, 184ralimdaa 2498 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1 → ∀𝑥𝐴 (𝑔𝑥) = 1o))
186177, 185orim12d 775 . . . . 5 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → ((∃𝑥𝐴 ((𝐺𝑔)‘𝑥) = 0 ∨ ∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1) → (∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)))
187152, 186mpd 13 . . . 4 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o))
188187ralrimiva 2505 . . 3 ((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) → ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o))
189105, 188impbida 585 . 2 (𝐴𝑉 → (∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o) ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)))
1901, 189bitrd 187 1 (𝐴𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697   = wceq 1331  ⊤wtru 1332   ∈ wcel 1480  ∀wral 2416  ∃wrex 2417  Vcvv 2686   ⊆ wss 3071  ∅c0 3363  {cpr 3528   ↦ cmpt 3989  suc csuc 4287  ωcom 4504  ◡ccnv 4538   ↾ cres 4541   ∘ ccom 4543   Fn wfn 5118  ⟶wf 5119  –1-1-onto→wf1o 5122  ‘cfv 5123  (class class class)co 5774  freccfrec 6287  1oc1o 6306  2oc2o 6307   ↑𝑚 cmap 6542  Omnicomni 7004  0cc0 7632  1c1 7633   + caddc 7635  ℕ0cn0 8989  ℤcz 9066 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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7723  ax-resscn 7724  ax-1cn 7725  ax-1re 7726  ax-icn 7727  ax-addcl 7728  ax-addrcl 7729  ax-mulcl 7730  ax-addcom 7732  ax-addass 7734  ax-distr 7736  ax-i2m1 7737  ax-0lt1 7738  ax-0id 7740  ax-rnegex 7741  ax-cnre 7743  ax-pre-ltirr 7744  ax-pre-ltwlin 7745  ax-pre-lttrn 7746  ax-pre-ltadd 7748 This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-recs 6202  df-frec 6288  df-1o 6313  df-2o 6314  df-map 6544  df-omni 7006  df-pnf 7814  df-mnf 7815  df-xr 7816  df-ltxr 7817  df-le 7818  df-sub 7947  df-neg 7948  df-inn 8733  df-n0 8990  df-z 9067  df-uz 9339 This theorem is referenced by:  isomninn  13287
 Copyright terms: Public domain W3C validator