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

Theorem isomninnlem 12917
Description: Lemma for isomninn 12918. 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 6959 . 2 (𝐴𝑉 → (𝐴 ∈ Omni ↔ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)))
2 fveq1 5374 . . . . . . . . 9 (𝑔 = (𝐺𝑓) → (𝑔𝑥) = ((𝐺𝑓)‘𝑥))
32eqeq1d 2123 . . . . . . . 8 (𝑔 = (𝐺𝑓) → ((𝑔𝑥) = ∅ ↔ ((𝐺𝑓)‘𝑥) = ∅))
43rexbidv 2412 . . . . . . 7 (𝑔 = (𝐺𝑓) → (∃𝑥𝐴 (𝑔𝑥) = ∅ ↔ ∃𝑥𝐴 ((𝐺𝑓)‘𝑥) = ∅))
52eqeq1d 2123 . . . . . . . 8 (𝑔 = (𝐺𝑓) → ((𝑔𝑥) = 1o ↔ ((𝐺𝑓)‘𝑥) = 1o))
65ralbidv 2411 . . . . . . 7 (𝑔 = (𝐺𝑓) → (∀𝑥𝐴 (𝑔𝑥) = 1o ↔ ∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o))
74, 6orbi12d 765 . . . . . 6 (𝑔 = (𝐺𝑓) → ((∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o) ↔ (∃𝑥𝐴 ((𝐺𝑓)‘𝑥) = ∅ ∨ ∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o)))
8 simplr 502 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o))
9 isomninnlem.g . . . . . . . . . . . . 13 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
109frechashgf1o 10094 . . . . . . . . . . . 12 𝐺:ω–1-1-onto→ℕ0
11 f1ocnv 5336 . . . . . . . . . . . 12 (𝐺:ω–1-1-onto→ℕ0𝐺:ℕ01-1-onto→ω)
12 f1of 5323 . . . . . . . . . . . 12 (𝐺:ℕ01-1-onto→ω → 𝐺:ℕ0⟶ω)
1310, 11, 12mp2b 8 . . . . . . . . . . 11 𝐺:ℕ0⟶ω
14 0nn0 8896 . . . . . . . . . . . 12 0 ∈ ℕ0
15 1nn0 8897 . . . . . . . . . . . 12 1 ∈ ℕ0
16 prssi 3644 . . . . . . . . . . . 12 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
1714, 15, 16mp2an 420 . . . . . . . . . . 11 {0, 1} ⊆ ℕ0
18 fssres 5256 . . . . . . . . . . 11 ((𝐺:ℕ0⟶ω ∧ {0, 1} ⊆ ℕ0) → (𝐺 ↾ {0, 1}):{0, 1}⟶ω)
1913, 17, 18mp2an 420 . . . . . . . . . 10 (𝐺 ↾ {0, 1}):{0, 1}⟶ω
20 ffn 5230 . . . . . . . . . 10 ((𝐺 ↾ {0, 1}):{0, 1}⟶ω → (𝐺 ↾ {0, 1}) Fn {0, 1})
2119, 20ax-mp 7 . . . . . . . . 9 (𝐺 ↾ {0, 1}) Fn {0, 1}
22 fvres 5399 . . . . . . . . . . 11 (𝑗 ∈ {0, 1} → ((𝐺 ↾ {0, 1})‘𝑗) = (𝐺𝑗))
23 elpri 3516 . . . . . . . . . . . 12 (𝑗 ∈ {0, 1} → (𝑗 = 0 ∨ 𝑗 = 1))
24 fveq2 5375 . . . . . . . . . . . . . 14 (𝑗 = 0 → (𝐺𝑗) = (𝐺‘0))
25 0zd 8970 . . . . . . . . . . . . . . . . . 18 (⊤ → 0 ∈ ℤ)
2625, 9frec2uz0d 10065 . . . . . . . . . . . . . . . . 17 (⊤ → (𝐺‘∅) = 0)
2726mptru 1323 . . . . . . . . . . . . . . . 16 (𝐺‘∅) = 0
28 peano1 4468 . . . . . . . . . . . . . . . . 17 ∅ ∈ ω
29 f1ocnvfv 5634 . . . . . . . . . . . . . . . . 17 ((𝐺:ω–1-1-onto→ℕ0 ∧ ∅ ∈ ω) → ((𝐺‘∅) = 0 → (𝐺‘0) = ∅))
3010, 28, 29mp2an 420 . . . . . . . . . . . . . . . 16 ((𝐺‘∅) = 0 → (𝐺‘0) = ∅)
3127, 30ax-mp 7 . . . . . . . . . . . . . . 15 (𝐺‘0) = ∅
32 0lt2o 6292 . . . . . . . . . . . . . . 15 ∅ ∈ 2o
3331, 32eqeltri 2187 . . . . . . . . . . . . . 14 (𝐺‘0) ∈ 2o
3424, 33syl6eqel 2205 . . . . . . . . . . . . 13 (𝑗 = 0 → (𝐺𝑗) ∈ 2o)
35 fveq2 5375 . . . . . . . . . . . . . 14 (𝑗 = 1 → (𝐺𝑗) = (𝐺‘1))
36 df-1o 6267 . . . . . . . . . . . . . . . . . 18 1o = suc ∅
3736fveq2i 5378 . . . . . . . . . . . . . . . . 17 (𝐺‘1o) = (𝐺‘suc ∅)
3828a1i 9 . . . . . . . . . . . . . . . . . . 19 (⊤ → ∅ ∈ ω)
3925, 9, 38frec2uzsucd 10067 . . . . . . . . . . . . . . . . . 18 (⊤ → (𝐺‘suc ∅) = ((𝐺‘∅) + 1))
4039mptru 1323 . . . . . . . . . . . . . . . . 17 (𝐺‘suc ∅) = ((𝐺‘∅) + 1)
4127oveq1i 5738 . . . . . . . . . . . . . . . . . 18 ((𝐺‘∅) + 1) = (0 + 1)
42 0p1e1 8744 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
4341, 42eqtri 2135 . . . . . . . . . . . . . . . . 17 ((𝐺‘∅) + 1) = 1
4437, 40, 433eqtri 2139 . . . . . . . . . . . . . . . 16 (𝐺‘1o) = 1
45 1onn 6370 . . . . . . . . . . . . . . . . 17 1o ∈ ω
46 f1ocnvfv 5634 . . . . . . . . . . . . . . . . 17 ((𝐺:ω–1-1-onto→ℕ0 ∧ 1o ∈ ω) → ((𝐺‘1o) = 1 → (𝐺‘1) = 1o))
4710, 45, 46mp2an 420 . . . . . . . . . . . . . . . 16 ((𝐺‘1o) = 1 → (𝐺‘1) = 1o)
4844, 47ax-mp 7 . . . . . . . . . . . . . . 15 (𝐺‘1) = 1o
49 1lt2o 6293 . . . . . . . . . . . . . . 15 1o ∈ 2o
5048, 49eqeltri 2187 . . . . . . . . . . . . . 14 (𝐺‘1) ∈ 2o
5135, 50syl6eqel 2205 . . . . . . . . . . . . 13 (𝑗 = 1 → (𝐺𝑗) ∈ 2o)
5234, 51jaoi 688 . . . . . . . . . . . 12 ((𝑗 = 0 ∨ 𝑗 = 1) → (𝐺𝑗) ∈ 2o)
5323, 52syl 14 . . . . . . . . . . 11 (𝑗 ∈ {0, 1} → (𝐺𝑗) ∈ 2o)
5422, 53eqeltrd 2191 . . . . . . . . . 10 (𝑗 ∈ {0, 1} → ((𝐺 ↾ {0, 1})‘𝑗) ∈ 2o)
5554rgen 2459 . . . . . . . . 9 𝑗 ∈ {0, 1} ((𝐺 ↾ {0, 1})‘𝑗) ∈ 2o
56 ffnfv 5532 . . . . . . . . 9 ((𝐺 ↾ {0, 1}):{0, 1}⟶2o ↔ ((𝐺 ↾ {0, 1}) Fn {0, 1} ∧ ∀𝑗 ∈ {0, 1} ((𝐺 ↾ {0, 1})‘𝑗) ∈ 2o))
5721, 55, 56mpbir2an 909 . . . . . . . 8 (𝐺 ↾ {0, 1}):{0, 1}⟶2o
58 elmapi 6518 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
5958adantl 273 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝑓:𝐴⟶{0, 1})
60 fco2 5247 . . . . . . . 8 (((𝐺 ↾ {0, 1}):{0, 1}⟶2o𝑓:𝐴⟶{0, 1}) → (𝐺𝑓):𝐴⟶2o)
6157, 59, 60sylancr 408 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝐺𝑓):𝐴⟶2o)
62 2onn 6371 . . . . . . . . 9 2o ∈ ω
6362a1i 9 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 2o ∈ ω)
64 simpll 501 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝐴𝑉)
6563, 64elmapd 6510 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ((𝐺𝑓) ∈ (2o𝑚 𝐴) ↔ (𝐺𝑓):𝐴⟶2o))
6661, 65mpbird 166 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝐺𝑓) ∈ (2o𝑚 𝐴))
677, 8, 66rspcdva 2765 . . . . 5 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∃𝑥𝐴 ((𝐺𝑓)‘𝑥) = ∅ ∨ ∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o))
68 nfv 1491 . . . . . . . . 9 𝑥 𝐴𝑉
69 nfcv 2255 . . . . . . . . . 10 𝑥(2o𝑚 𝐴)
70 nfre1 2450 . . . . . . . . . . 11 𝑥𝑥𝐴 (𝑔𝑥) = ∅
71 nfra1 2440 . . . . . . . . . . 11 𝑥𝑥𝐴 (𝑔𝑥) = 1o
7270, 71nfor 1536 . . . . . . . . . 10 𝑥(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)
7369, 72nfralxy 2445 . . . . . . . . 9 𝑥𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)
7468, 73nfan 1527 . . . . . . . 8 𝑥(𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o))
75 nfv 1491 . . . . . . . 8 𝑥 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)
7674, 75nfan 1527 . . . . . . 7 𝑥((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴))
77 simplr 502 . . . . . . . . . . . . . 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 5510 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ {0, 1})
8117, 80sseldi 3061 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ℕ0)
82 f1ocnvfv2 5633 . . . . . . . . . . 11 ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑓𝑥) ∈ ℕ0) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝑓𝑥))
8310, 81, 82sylancr 408 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝑓𝑥))
8483adantr 272 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝑓𝑥))
85 fvco3 5446 . . . . . . . . . . . . . 14 ((𝑓:𝐴⟶{0, 1} ∧ 𝑥𝐴) → ((𝐺𝑓)‘𝑥) = (𝐺‘(𝑓𝑥)))
8678, 85sylancom 414 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝐺𝑓)‘𝑥) = (𝐺‘(𝑓𝑥)))
8786eqeq1d 2123 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑓)‘𝑥) = ∅ ↔ (𝐺‘(𝑓𝑥)) = ∅))
8887biimpa 292 . . . . . . . . . . 11 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝐺‘(𝑓𝑥)) = ∅)
8988fveq2d 5379 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝐺‘∅))
9089, 27syl6eq 2163 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝐺‘(𝐺‘(𝑓𝑥))) = 0)
9184, 90eqtr3d 2149 . . . . . . . 8 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = ∅) → (𝑓𝑥) = 0)
9291exp31 359 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝑥𝐴 → (((𝐺𝑓)‘𝑥) = ∅ → (𝑓𝑥) = 0)))
9376, 92reximdai 2504 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∃𝑥𝐴 ((𝐺𝑓)‘𝑥) = ∅ → ∃𝑥𝐴 (𝑓𝑥) = 0))
9483adantr 272 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝑓𝑥))
9586adantr 272 . . . . . . . . . . . 12 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → ((𝐺𝑓)‘𝑥) = (𝐺‘(𝑓𝑥)))
96 simpr 109 . . . . . . . . . . . 12 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → ((𝐺𝑓)‘𝑥) = 1o)
9795, 96eqtr3d 2149 . . . . . . . . . . 11 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝐺‘(𝑓𝑥)) = 1o)
9897fveq2d 5379 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝐺‘(𝐺‘(𝑓𝑥))) = (𝐺‘1o))
9998, 44syl6eq 2163 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝐺‘(𝐺‘(𝑓𝑥))) = 1)
10094, 99eqtr3d 2149 . . . . . . . 8 (((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑓)‘𝑥) = 1o) → (𝑓𝑥) = 1)
101100ex 114 . . . . . . 7 ((((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑓)‘𝑥) = 1o → (𝑓𝑥) = 1))
10276, 101ralimdaa 2472 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o → ∀𝑥𝐴 (𝑓𝑥) = 1))
10393, 102orim12d 758 . . . . 5 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ((∃𝑥𝐴 ((𝐺𝑓)‘𝑥) = ∅ ∨ ∀𝑥𝐴 ((𝐺𝑓)‘𝑥) = 1o) → (∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)))
10467, 103mpd 13 . . . 4 (((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1))
105104ralrimiva 2479 . . 3 ((𝐴𝑉 ∧ ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1))
106 fveq1 5374 . . . . . . . . 9 (𝑓 = (𝐺𝑔) → (𝑓𝑥) = ((𝐺𝑔)‘𝑥))
107106eqeq1d 2123 . . . . . . . 8 (𝑓 = (𝐺𝑔) → ((𝑓𝑥) = 0 ↔ ((𝐺𝑔)‘𝑥) = 0))
108107rexbidv 2412 . . . . . . 7 (𝑓 = (𝐺𝑔) → (∃𝑥𝐴 (𝑓𝑥) = 0 ↔ ∃𝑥𝐴 ((𝐺𝑔)‘𝑥) = 0))
109106eqeq1d 2123 . . . . . . . 8 (𝑓 = (𝐺𝑔) → ((𝑓𝑥) = 1 ↔ ((𝐺𝑔)‘𝑥) = 1))
110109ralbidv 2411 . . . . . . 7 (𝑓 = (𝐺𝑔) → (∀𝑥𝐴 (𝑓𝑥) = 1 ↔ ∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1))
111108, 110orbi12d 765 . . . . . 6 (𝑓 = (𝐺𝑔) → ((∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1) ↔ (∃𝑥𝐴 ((𝐺𝑔)‘𝑥) = 0 ∨ ∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1)))
112 simplr 502 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1))
113 f1of 5323 . . . . . . . . . . . 12 (𝐺:ω–1-1-onto→ℕ0𝐺:ω⟶ℕ0)
11410, 113ax-mp 7 . . . . . . . . . . 11 𝐺:ω⟶ℕ0
115 omelon 4482 . . . . . . . . . . . . 13 ω ∈ On
116115onelssi 4311 . . . . . . . . . . . 12 (2o ∈ ω → 2o ⊆ ω)
11762, 116ax-mp 7 . . . . . . . . . . 11 2o ⊆ ω
118 fssres 5256 . . . . . . . . . . 11 ((𝐺:ω⟶ℕ0 ∧ 2o ⊆ ω) → (𝐺 ↾ 2o):2o⟶ℕ0)
119114, 117, 118mp2an 420 . . . . . . . . . 10 (𝐺 ↾ 2o):2o⟶ℕ0
120 ffn 5230 . . . . . . . . . 10 ((𝐺 ↾ 2o):2o⟶ℕ0 → (𝐺 ↾ 2o) Fn 2o)
121119, 120ax-mp 7 . . . . . . . . 9 (𝐺 ↾ 2o) Fn 2o
122 fvres 5399 . . . . . . . . . . 11 (𝑗 ∈ 2o → ((𝐺 ↾ 2o)‘𝑗) = (𝐺𝑗))
123 elpri 3516 . . . . . . . . . . . . 13 (𝑗 ∈ {∅, 1o} → (𝑗 = ∅ ∨ 𝑗 = 1o))
124 df2o3 6281 . . . . . . . . . . . . 13 2o = {∅, 1o}
125123, 124eleq2s 2209 . . . . . . . . . . . 12 (𝑗 ∈ 2o → (𝑗 = ∅ ∨ 𝑗 = 1o))
126 fveq2 5375 . . . . . . . . . . . . . 14 (𝑗 = ∅ → (𝐺𝑗) = (𝐺‘∅))
127 c0ex 7684 . . . . . . . . . . . . . . . 16 0 ∈ V
128127prid1 3595 . . . . . . . . . . . . . . 15 0 ∈ {0, 1}
12927, 128eqeltri 2187 . . . . . . . . . . . . . 14 (𝐺‘∅) ∈ {0, 1}
130126, 129syl6eqel 2205 . . . . . . . . . . . . 13 (𝑗 = ∅ → (𝐺𝑗) ∈ {0, 1})
131 fveq2 5375 . . . . . . . . . . . . . 14 (𝑗 = 1o → (𝐺𝑗) = (𝐺‘1o))
132 1ex 7685 . . . . . . . . . . . . . . . 16 1 ∈ V
133132prid2 3596 . . . . . . . . . . . . . . 15 1 ∈ {0, 1}
13444, 133eqeltri 2187 . . . . . . . . . . . . . 14 (𝐺‘1o) ∈ {0, 1}
135131, 134syl6eqel 2205 . . . . . . . . . . . . 13 (𝑗 = 1o → (𝐺𝑗) ∈ {0, 1})
136130, 135jaoi 688 . . . . . . . . . . . 12 ((𝑗 = ∅ ∨ 𝑗 = 1o) → (𝐺𝑗) ∈ {0, 1})
137125, 136syl 14 . . . . . . . . . . 11 (𝑗 ∈ 2o → (𝐺𝑗) ∈ {0, 1})
138122, 137eqeltrd 2191 . . . . . . . . . 10 (𝑗 ∈ 2o → ((𝐺 ↾ 2o)‘𝑗) ∈ {0, 1})
139138rgen 2459 . . . . . . . . 9 𝑗 ∈ 2o ((𝐺 ↾ 2o)‘𝑗) ∈ {0, 1}
140 ffnfv 5532 . . . . . . . . 9 ((𝐺 ↾ 2o):2o⟶{0, 1} ↔ ((𝐺 ↾ 2o) Fn 2o ∧ ∀𝑗 ∈ 2o ((𝐺 ↾ 2o)‘𝑗) ∈ {0, 1}))
141121, 139, 140mpbir2an 909 . . . . . . . 8 (𝐺 ↾ 2o):2o⟶{0, 1}
142 elmapi 6518 . . . . . . . . 9 (𝑔 ∈ (2o𝑚 𝐴) → 𝑔:𝐴⟶2o)
143142adantl 273 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → 𝑔:𝐴⟶2o)
144 fco2 5247 . . . . . . . 8 (((𝐺 ↾ 2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺𝑔):𝐴⟶{0, 1})
145141, 143, 144sylancr 408 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝐺𝑔):𝐴⟶{0, 1})
146 prexg 4093 . . . . . . . . . 10 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ∈ V)
14714, 15, 146mp2an 420 . . . . . . . . 9 {0, 1} ∈ V
148147a1i 9 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → {0, 1} ∈ V)
149 simpll 501 . . . . . . . 8 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → 𝐴𝑉)
150148, 149elmapd 6510 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → ((𝐺𝑔) ∈ ({0, 1} ↑𝑚 𝐴) ↔ (𝐺𝑔):𝐴⟶{0, 1}))
151145, 150mpbird 166 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝐺𝑔) ∈ ({0, 1} ↑𝑚 𝐴))
152111, 112, 151rspcdva 2765 . . . . 5 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∃𝑥𝐴 ((𝐺𝑔)‘𝑥) = 0 ∨ ∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1))
153 nfcv 2255 . . . . . . . . . 10 𝑥({0, 1} ↑𝑚 𝐴)
154 nfre1 2450 . . . . . . . . . . 11 𝑥𝑥𝐴 (𝑓𝑥) = 0
155 nfra1 2440 . . . . . . . . . . 11 𝑥𝑥𝐴 (𝑓𝑥) = 1
156154, 155nfor 1536 . . . . . . . . . 10 𝑥(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)
157153, 156nfralxy 2445 . . . . . . . . 9 𝑥𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)
15868, 157nfan 1527 . . . . . . . 8 𝑥(𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1))
159 nfv 1491 . . . . . . . 8 𝑥 𝑔 ∈ (2o𝑚 𝐴)
160158, 159nfan 1527 . . . . . . 7 𝑥((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴))
161143adantr 272 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑔:𝐴⟶2o)
162117a1i 9 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 2o ⊆ ω)
163161, 162fssd 5243 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑔:𝐴⟶ω)
164 simpr 109 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → 𝑥𝐴)
165163, 164ffvelrnd 5510 . . . . . . . . . . 11 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝑔𝑥) ∈ ω)
166 f1ocnvfv1 5632 . . . . . . . . . . 11 ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑔𝑥) ∈ ω) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝑔𝑥))
16710, 165, 166sylancr 408 . . . . . . . . . 10 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝑔𝑥))
168167adantr 272 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝑔𝑥))
169 fvco3 5446 . . . . . . . . . . . . . 14 ((𝑔:𝐴⟶2o𝑥𝐴) → ((𝐺𝑔)‘𝑥) = (𝐺‘(𝑔𝑥)))
170161, 169sylancom 414 . . . . . . . . . . . . 13 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → ((𝐺𝑔)‘𝑥) = (𝐺‘(𝑔𝑥)))
171170eqeq1d 2123 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑔)‘𝑥) = 0 ↔ (𝐺‘(𝑔𝑥)) = 0))
172171biimpa 292 . . . . . . . . . . 11 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝐺‘(𝑔𝑥)) = 0)
173172fveq2d 5379 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝐺‘0))
174173, 31syl6eq 2163 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝐺‘(𝐺‘(𝑔𝑥))) = ∅)
175168, 174eqtr3d 2149 . . . . . . . 8 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 0) → (𝑔𝑥) = ∅)
176175exp31 359 . . . . . . 7 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (𝑥𝐴 → (((𝐺𝑔)‘𝑥) = 0 → (𝑔𝑥) = ∅)))
177160, 176reximdai 2504 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∃𝑥𝐴 ((𝐺𝑔)‘𝑥) = 0 → ∃𝑥𝐴 (𝑔𝑥) = ∅))
178167adantr 272 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝑔𝑥))
179170eqeq1d 2123 . . . . . . . . . . . 12 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔𝑥)) = 1))
180179biimpa 292 . . . . . . . . . . 11 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝐺‘(𝑔𝑥)) = 1)
181180fveq2d 5379 . . . . . . . . . 10 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝐺‘(𝐺‘(𝑔𝑥))) = (𝐺‘1))
182181, 48syl6eq 2163 . . . . . . . . 9 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝐺‘(𝐺‘(𝑔𝑥))) = 1o)
183178, 182eqtr3d 2149 . . . . . . . 8 (((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) ∧ ((𝐺𝑔)‘𝑥) = 1) → (𝑔𝑥) = 1o)
184183ex 114 . . . . . . 7 ((((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) ∧ 𝑥𝐴) → (((𝐺𝑔)‘𝑥) = 1 → (𝑔𝑥) = 1o))
185160, 184ralimdaa 2472 . . . . . 6 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1 → ∀𝑥𝐴 (𝑔𝑥) = 1o))
186177, 185orim12d 758 . . . . 5 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → ((∃𝑥𝐴 ((𝐺𝑔)‘𝑥) = 0 ∨ ∀𝑥𝐴 ((𝐺𝑔)‘𝑥) = 1) → (∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o)))
187152, 186mpd 13 . . . 4 (((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) ∧ 𝑔 ∈ (2o𝑚 𝐴)) → (∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o))
188187ralrimiva 2479 . . 3 ((𝐴𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)) → ∀𝑔 ∈ (2o𝑚 𝐴)(∃𝑥𝐴 (𝑔𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑔𝑥) = 1o))
189105, 188impbida 568 . 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 680   = wceq 1314  wtru 1315  wcel 1463  wral 2390  wrex 2391  Vcvv 2657  wss 3037  c0 3329  {cpr 3494  cmpt 3949  suc csuc 4247  ωcom 4464  ccnv 4498  cres 4501  ccom 4503   Fn wfn 5076  wf 5077  1-1-ontowf1o 5080  cfv 5081  (class class class)co 5728  freccfrec 6241  1oc1o 6260  2oc2o 6261  𝑚 cmap 6496  Omnicomni 6954  0cc0 7547  1c1 7548   + caddc 7550  0cn0 8881  cz 8958
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4003  ax-sep 4006  ax-nul 4014  ax-pow 4058  ax-pr 4091  ax-un 4315  ax-setind 4412  ax-iinf 4462  ax-cnex 7636  ax-resscn 7637  ax-1cn 7638  ax-1re 7639  ax-icn 7640  ax-addcl 7641  ax-addrcl 7642  ax-mulcl 7643  ax-addcom 7645  ax-addass 7647  ax-distr 7649  ax-i2m1 7650  ax-0lt1 7651  ax-0id 7653  ax-rnegex 7654  ax-cnre 7656  ax-pre-ltirr 7657  ax-pre-ltwlin 7658  ax-pre-lttrn 7659  ax-pre-ltadd 7661
This theorem depends on definitions:  df-bi 116  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ne 2283  df-nel 2378  df-ral 2395  df-rex 2396  df-reu 2397  df-rab 2399  df-v 2659  df-sbc 2879  df-csb 2972  df-dif 3039  df-un 3041  df-in 3043  df-ss 3050  df-nul 3330  df-pw 3478  df-sn 3499  df-pr 3500  df-op 3502  df-uni 3703  df-int 3738  df-iun 3781  df-br 3896  df-opab 3950  df-mpt 3951  df-tr 3987  df-id 4175  df-iord 4248  df-on 4250  df-ilim 4251  df-suc 4253  df-iom 4465  df-xp 4505  df-rel 4506  df-cnv 4507  df-co 4508  df-dm 4509  df-rn 4510  df-res 4511  df-ima 4512  df-iota 5046  df-fun 5083  df-fn 5084  df-f 5085  df-f1 5086  df-fo 5087  df-f1o 5088  df-fv 5089  df-riota 5684  df-ov 5731  df-oprab 5732  df-mpo 5733  df-recs 6156  df-frec 6242  df-1o 6267  df-2o 6268  df-map 6498  df-omni 6956  df-pnf 7726  df-mnf 7727  df-xr 7728  df-ltxr 7729  df-le 7730  df-sub 7858  df-neg 7859  df-inn 8631  df-n0 8882  df-z 8959  df-uz 9229
This theorem is referenced by:  isomninn  12918
  Copyright terms: Public domain W3C validator