Theorem iswomninnlem 16328

Description: Lemma for iswomnimap 7301. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.)

Hypothesis

Ref	Expression
iswomninnlem.g	⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)

Assertion

Ref	Expression
iswomninnlem	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))

Distinct variable groups:   𝐴,𝑓,𝑥   𝑓,𝐺,𝑥   𝑓,𝑉,𝑥

Proof of Theorem iswomninnlem

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iswomnimap 7301	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
2		fveq1 5602	. . . . . . . . 9 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (𝑔‘𝑥) = ((◡𝐺 ∘ 𝑓)‘𝑥))
3	2	eqeq1d 2218	. . . . . . . 8 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = 1o ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
4	3	ralbidv 2510	. . . . . . 7 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
5	4	dcbid 842	. . . . . 6 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ DECID ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
6		simplr 528	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
7		iswomninnlem.g	. . . . . . . . . . 11 ⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
8	7	012of 16268	. . . . . . . . . 10 ⊢ (◡𝐺 ↾ {0, 1}):{0, 1}⟶2o
9		elmapi 6787	. . . . . . . . . 10 ⊢ (𝑓 ∈ ({0, 1} ↑𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
10		fco2 5466	. . . . . . . . . 10 ⊢ (((◡𝐺 ↾ {0, 1}):{0, 1}⟶2o ∧ 𝑓:𝐴⟶{0, 1}) → (◡𝐺 ∘ 𝑓):𝐴⟶2o)
11	8, 9, 10	sylancr 414	. . . . . . . . 9 ⊢ (𝑓 ∈ ({0, 1} ↑𝑚 𝐴) → (◡𝐺 ∘ 𝑓):𝐴⟶2o)
12	11	adantl 277	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (◡𝐺 ∘ 𝑓):𝐴⟶2o)
13		2onn 6637	. . . . . . . . . 10 ⊢ 2o ∈ ω
14	13	a1i 9	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 2o ∈ ω)
15		simpl 109	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝐴 ∈ 𝑉)
16	14, 15	elmapd 6779	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ((◡𝐺 ∘ 𝑓) ∈ (2o ↑𝑚 𝐴) ↔ (◡𝐺 ∘ 𝑓):𝐴⟶2o))
17	12, 16	mpbird 167	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (◡𝐺 ∘ 𝑓) ∈ (2o ↑𝑚 𝐴))
18	17	adantlr 477	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (◡𝐺 ∘ 𝑓) ∈ (2o ↑𝑚 𝐴))
19	5, 6, 18	rspcdva 2892	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → DECID ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)
20		nfv 1554	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑉
21		nfcv 2352	. . . . . . . . . 10 ⊢ Ⅎ𝑥(2o ↑𝑚 𝐴)
22		nfra1 2541	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
23	22	nfdc 1685	. . . . . . . . . 10 ⊢ Ⅎ𝑥DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
24	21, 23	nfralxy 2548	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
25	20, 24	nfan 1591	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
26		nfv 1554	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)
27	25, 26	nfan 1591	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴))
28	9	ad2antlr 489	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1})
29		fvco3 5678	. . . . . . . . . 10 ⊢ ((𝑓:𝐴⟶{0, 1} ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
30	28, 29	sylancom 420	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
31	30	eqeq1d 2218	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o))
32		df-1o 6532	. . . . . . . . . . . 12 ⊢ 1o = suc ∅
33	32	fveq2i 5606	. . . . . . . . . . 11 ⊢ (𝐺‘1o) = (𝐺‘suc ∅)
34		0zd 9426	. . . . . . . . . . . . 13 ⊢ (⊤ → 0 ∈ ℤ)
35		peano1 4663	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ ω
36	35	a1i 9	. . . . . . . . . . . . 13 ⊢ (⊤ → ∅ ∈ ω)
37	34, 7, 36	frec2uzsucd 10590	. . . . . . . . . . . 12 ⊢ (⊤ → (𝐺‘suc ∅) = ((𝐺‘∅) + 1))
38	37	mptru 1384	. . . . . . . . . . 11 ⊢ (𝐺‘suc ∅) = ((𝐺‘∅) + 1)
39	34, 7	frec2uz0d 10588	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝐺‘∅) = 0)
40	39	mptru 1384	. . . . . . . . . . . . 13 ⊢ (𝐺‘∅) = 0
41	40	oveq1i 5984	. . . . . . . . . . . 12 ⊢ ((𝐺‘∅) + 1) = (0 + 1)
42		0p1e1 9192	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
43	41, 42	eqtri 2230	. . . . . . . . . . 11 ⊢ ((𝐺‘∅) + 1) = 1
44	33, 38, 43	3eqtri 2234	. . . . . . . . . 10 ⊢ (𝐺‘1o) = 1
45	44	eqeq2i 2220	. . . . . . . . 9 ⊢ ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1)
46	7	frechashgf1o 10617	. . . . . . . . . . . . 13 ⊢ 𝐺:ω–1-1-onto→ℕ0
47		f1ocnv 5561	. . . . . . . . . . . . 13 ⊢ (𝐺:ω–1-1-onto→ℕ0 → ◡𝐺:ℕ0–1-1-onto→ω)
48		f1of 5548	. . . . . . . . . . . . 13 ⊢ (◡𝐺:ℕ0–1-1-onto→ω → ◡𝐺:ℕ0⟶ω)
49	46, 47, 48	mp2b 8	. . . . . . . . . . . 12 ⊢ ◡𝐺:ℕ0⟶ω
50	49	a1i 9	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ◡𝐺:ℕ0⟶ω)
51		0nn0 9352	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
52		1nn0 9353	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ0
53		prssi 3805	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
54	51, 52, 53	mp2an 426	. . . . . . . . . . . 12 ⊢ {0, 1} ⊆ ℕ0
55		simpr 110	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
56	28, 55	ffvelcdmd 5744	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1})
57	54, 56	sselid 3202	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℕ0)
58	50, 57	ffvelcdmd 5744	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝑓‘𝑥)) ∈ ω)
59		1onn 6636	. . . . . . . . . . 11 ⊢ 1o ∈ ω
60		f1of1 5547	. . . . . . . . . . . . 13 ⊢ (𝐺:ω–1-1-onto→ℕ0 → 𝐺:ω–1-1→ℕ0)
61	46, 60	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝐺:ω–1-1→ℕ0
62		f1fveq 5869	. . . . . . . . . . . 12 ⊢ ((𝐺:ω–1-1→ℕ0 ∧ ((◡𝐺‘(𝑓‘𝑥)) ∈ ω ∧ 1o ∈ ω)) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o))
63	61, 62	mpan 424	. . . . . . . . . . 11 ⊢ (((◡𝐺‘(𝑓‘𝑥)) ∈ ω ∧ 1o ∈ ω) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o))
64	59, 63	mpan2 425	. . . . . . . . . 10 ⊢ ((◡𝐺‘(𝑓‘𝑥)) ∈ ω → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o))
65	58, 64	syl 14	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o))
66	45, 65	bitr3id 194	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1 ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o))
67		f1ocnvfv2 5875	. . . . . . . . . 10 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑓‘𝑥) ∈ ℕ0) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
68	46, 57, 67	sylancr 414	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
69	68	eqeq1d 2218	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1 ↔ (𝑓‘𝑥) = 1))
70	31, 66, 69	3bitr2d 216	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ (𝑓‘𝑥) = 1))
71	27, 70	ralbida 2504	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
72	71	dcbid 842	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (DECID ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
73	19, 72	mpbid 147	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
74	73	ralrimiva 2583	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
75		fveq1 5602	. . . . . . . . 9 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (𝑓‘𝑥) = ((𝐺 ∘ 𝑔)‘𝑥))
76	75	eqeq1d 2218	. . . . . . . 8 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 1 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 1))
77	76	ralbidv 2510	. . . . . . 7 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
78	77	dcbid 842	. . . . . 6 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ DECID ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
79		simplr 528	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
80	7	2o01f 16269	. . . . . . . 8 ⊢ (𝐺 ↾ 2o):2o⟶{0, 1}
81		elmapi 6787	. . . . . . . . 9 ⊢ (𝑔 ∈ (2o ↑𝑚 𝐴) → 𝑔:𝐴⟶2o)
82	81	adantl 277	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → 𝑔:𝐴⟶2o)
83		fco2 5466	. . . . . . . 8 ⊢ (((𝐺 ↾ 2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
84	80, 82, 83	sylancr 414	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
85		prexg 4274	. . . . . . . . . 10 ⊢ ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ∈ V)
86	51, 52, 85	mp2an 426	. . . . . . . . 9 ⊢ {0, 1} ∈ V
87	86	a1i 9	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → {0, 1} ∈ V)
88		simpll 527	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → 𝐴 ∈ 𝑉)
89	87, 88	elmapd 6779	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → ((𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚 𝐴) ↔ (𝐺 ∘ 𝑔):𝐴⟶{0, 1}))
90	84, 89	mpbird 167	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚 𝐴))
91	78, 79, 90	rspcdva 2892	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → DECID ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1)
92		nfcv 2352	. . . . . . . . . 10 ⊢ Ⅎ𝑥({0, 1} ↑𝑚 𝐴)
93		nfra1 2541	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
94	93	nfdc 1685	. . . . . . . . . 10 ⊢ Ⅎ𝑥DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
95	92, 94	nfralxy 2548	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
96	20, 95	nfan 1591	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
97		nfv 1554	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑔 ∈ (2o ↑𝑚 𝐴)
98	96, 97	nfan 1591	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴))
99	81	ad2antlr 489	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶2o)
100		fvco3 5678	. . . . . . . . . 10 ⊢ ((𝑔:𝐴⟶2o ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
101	99, 100	sylancom 420	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
102	101	eqeq1d 2218	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔‘𝑥)) = 1))
103		f1of 5548	. . . . . . . . . . 11 ⊢ (𝐺:ω–1-1-onto→ℕ0 → 𝐺:ω⟶ℕ0)
104	46, 103	mp1i 10	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝐺:ω⟶ℕ0)
105		omelon 4678	. . . . . . . . . . . . . 14 ⊢ ω ∈ On
106	105	onelssi 4497	. . . . . . . . . . . . 13 ⊢ (2o ∈ ω → 2o ⊆ ω)
107	13, 106	mp1i 10	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 2o ⊆ ω)
108	99, 107	fssd 5462	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶ω)
109		simpr 110	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
110	108, 109	ffvelcdmd 5744	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ω)
111	104, 110	ffvelcdmd 5744	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(𝑔‘𝑥)) ∈ ℕ0)
112		f1ocnvfv 5876	. . . . . . . . . . . . 13 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ 1o ∈ ω) → ((𝐺‘1o) = 1 → (◡𝐺‘1) = 1o))
113	46, 59, 112	mp2an 426	. . . . . . . . . . . 12 ⊢ ((𝐺‘1o) = 1 → (◡𝐺‘1) = 1o)
114	44, 113	ax-mp 5	. . . . . . . . . . 11 ⊢ (◡𝐺‘1) = 1o
115	114	eqeq2i 2220	. . . . . . . . . 10 ⊢ ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1) ↔ (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o)
116		f1of1 5547	. . . . . . . . . . . . 13 ⊢ (◡𝐺:ℕ0–1-1-onto→ω → ◡𝐺:ℕ0–1-1→ω)
117	46, 47, 116	mp2b 8	. . . . . . . . . . . 12 ⊢ ◡𝐺:ℕ0–1-1→ω
118		f1fveq 5869	. . . . . . . . . . . 12 ⊢ ((◡𝐺:ℕ0–1-1→ω ∧ ((𝐺‘(𝑔‘𝑥)) ∈ ℕ0 ∧ 1 ∈ ℕ0)) → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1) ↔ (𝐺‘(𝑔‘𝑥)) = 1))
119	117, 118	mpan 424	. . . . . . . . . . 11 ⊢ (((𝐺‘(𝑔‘𝑥)) ∈ ℕ0 ∧ 1 ∈ ℕ0) → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1) ↔ (𝐺‘(𝑔‘𝑥)) = 1))
120	52, 119	mpan2 425	. . . . . . . . . 10 ⊢ ((𝐺‘(𝑔‘𝑥)) ∈ ℕ0 → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1) ↔ (𝐺‘(𝑔‘𝑥)) = 1))
121	115, 120	bitr3id 194	. . . . . . . . 9 ⊢ ((𝐺‘(𝑔‘𝑥)) ∈ ℕ0 → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o ↔ (𝐺‘(𝑔‘𝑥)) = 1))
122	111, 121	syl 14	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o ↔ (𝐺‘(𝑔‘𝑥)) = 1))
123		f1ocnvfv1 5874	. . . . . . . . . 10 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑔‘𝑥) ∈ ω) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
124	46, 110, 123	sylancr 414	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
125	124	eqeq1d 2218	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o ↔ (𝑔‘𝑥) = 1o))
126	102, 122, 125	3bitr2d 216	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ (𝑔‘𝑥) = 1o))
127	98, 126	ralbida 2504	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
128	127	dcbid 842	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (DECID ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
129	91, 128	mpbid 147	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
130	129	ralrimiva 2583	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
131	74, 130	impbida 598	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
132	1, 131	bitrd 188	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  DECID wdc 838   = wceq 1375  ⊤wtru 1376   ∈ wcel 2180  ∀wral 2488  Vcvv 2779   ⊆ wss 3177  ∅c0 3471  {cpr 3647   ↦ cmpt 4124  suc csuc 4433  ωcom 4659  ^◡ccnv 4695   ↾ cres 4698   ∘ ccom 4700  ⟶wf 5290  –1-1→wf1 5291  –1-1-onto→wf1o 5293  ‘cfv 5294  (class class class)co 5974  freccfrec 6506  1_oc1o 6525  2_oc2o 6526   ↑_𝑚 cmap 6765  WOmnicwomni 7298  0cc0 7967  1c1 7968   + caddc 7970  ℕ₀cn0 9337  ℤcz 9414

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 617  ax-in2 618  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-coll 4178  ax-sep 4181  ax-nul 4189  ax-pow 4237  ax-pr 4272  ax-un 4501  ax-setind 4606  ax-iinf 4657  ax-cnex 8058  ax-resscn 8059  ax-1cn 8060  ax-1re 8061  ax-icn 8062  ax-addcl 8063  ax-addrcl 8064  ax-mulcl 8065  ax-addcom 8067  ax-addass 8069  ax-distr 8071  ax-i2m1 8072  ax-0lt1 8073  ax-0id 8075  ax-rnegex 8076  ax-cnre 8078  ax-pre-ltirr 8079  ax-pre-ltwlin 8080  ax-pre-lttrn 8081  ax-pre-ltadd 8083

This theorem depends on definitions:  df-bi 117  df-dc 839  df-3or 984  df-3an 985  df-tru 1378  df-fal 1381  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ne 2381  df-nel 2476  df-ral 2493  df-rex 2494  df-reu 2495  df-rab 2497  df-v 2781  df-sbc 3009  df-csb 3105  df-dif 3179  df-un 3181  df-in 3183  df-ss 3190  df-nul 3472  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-int 3903  df-iun 3946  df-br 4063  df-opab 4125  df-mpt 4126  df-tr 4162  df-id 4361  df-iord 4434  df-on 4436  df-ilim 4437  df-suc 4439  df-iom 4660  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-iota 5254  df-fun 5296  df-fn 5297  df-f 5298  df-f1 5299  df-fo 5300  df-f1o 5301  df-fv 5302  df-riota 5927  df-ov 5977  df-oprab 5978  df-mpo 5979  df-recs 6421  df-frec 6507  df-1o 6532  df-2o 6533  df-map 6767  df-womni 7299  df-pnf 8151  df-mnf 8152  df-xr 8153  df-ltxr 8154  df-le 8155  df-sub 8287  df-neg 8288  df-inn 9079  df-n0 9338  df-z 9415  df-uz 9691

This theorem is referenced by:  iswomninn  16329