Theorem iswomninnlem 16721

Description: Lemma for iswomnimap 7370. 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 7370	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
2		fveq1 5641	. . . . . . . . 9 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (𝑔‘𝑥) = ((◡𝐺 ∘ 𝑓)‘𝑥))
3	2	eqeq1d 2239	. . . . . . . 8 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = 1o ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
4	3	ralbidv 2531	. . . . . . 7 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
5	4	dcbid 845	. . . . . 6 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ DECID ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
6		simplr 529	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
7		iswomninnlem.g	. . . . . . . . . . 11 ⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
8	7	012of 16652	. . . . . . . . . 10 ⊢ (◡𝐺 ↾ {0, 1}):{0, 1}⟶2o
9		elmapi 6844	. . . . . . . . . 10 ⊢ (𝑓 ∈ ({0, 1} ↑𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
10		fco2 5503	. . . . . . . . . 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 6694	. . . . . . . . . 10 ⊢ 2o ∈ ω
14	13	a1i 9	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 2o ∈ ω)
15		simpl 109	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝐴 ∈ 𝑉)
16	14, 15	elmapd 6836	. . . . . . . 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 2914	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → DECID ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)
20		nfv 1576	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑉
21		nfcv 2373	. . . . . . . . . 10 ⊢ Ⅎ𝑥(2o ↑𝑚 𝐴)
22		nfra1 2562	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
23	22	nfdc 1706	. . . . . . . . . 10 ⊢ Ⅎ𝑥DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
24	21, 23	nfralxy 2569	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
25	20, 24	nfan 1613	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
26		nfv 1576	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)
27	25, 26	nfan 1613	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴))
28	9	ad2antlr 489	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1})
29		fvco3 5720	. . . . . . . . . 10 ⊢ ((𝑓:𝐴⟶{0, 1} ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
30	28, 29	sylancom 420	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
31	30	eqeq1d 2239	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o))
32		df-1o 6587	. . . . . . . . . . . 12 ⊢ 1o = suc ∅
33	32	fveq2i 5645	. . . . . . . . . . 11 ⊢ (𝐺‘1o) = (𝐺‘suc ∅)
34		0zd 9496	. . . . . . . . . . . . 13 ⊢ (⊤ → 0 ∈ ℤ)
35		peano1 4694	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ ω
36	35	a1i 9	. . . . . . . . . . . . 13 ⊢ (⊤ → ∅ ∈ ω)
37	34, 7, 36	frec2uzsucd 10669	. . . . . . . . . . . 12 ⊢ (⊤ → (𝐺‘suc ∅) = ((𝐺‘∅) + 1))
38	37	mptru 1406	. . . . . . . . . . 11 ⊢ (𝐺‘suc ∅) = ((𝐺‘∅) + 1)
39	34, 7	frec2uz0d 10667	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝐺‘∅) = 0)
40	39	mptru 1406	. . . . . . . . . . . . 13 ⊢ (𝐺‘∅) = 0
41	40	oveq1i 6033	. . . . . . . . . . . 12 ⊢ ((𝐺‘∅) + 1) = (0 + 1)
42		0p1e1 9262	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
43	41, 42	eqtri 2251	. . . . . . . . . . 11 ⊢ ((𝐺‘∅) + 1) = 1
44	33, 38, 43	3eqtri 2255	. . . . . . . . . 10 ⊢ (𝐺‘1o) = 1
45	44	eqeq2i 2241	. . . . . . . . 9 ⊢ ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1)
46	7	frechashgf1o 10696	. . . . . . . . . . . . 13 ⊢ 𝐺:ω–1-1-onto→ℕ0
47		f1ocnv 5599	. . . . . . . . . . . . 13 ⊢ (𝐺:ω–1-1-onto→ℕ0 → ◡𝐺:ℕ0–1-1-onto→ω)
48		f1of 5586	. . . . . . . . . . . . 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 9422	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
52		1nn0 9423	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ0
53		prssi 3832	. . . . . . . . . . . . 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 5786	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1})
57	54, 56	sselid 3224	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℕ0)
58	50, 57	ffvelcdmd 5786	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝑓‘𝑥)) ∈ ω)
59		1onn 6693	. . . . . . . . . . 11 ⊢ 1o ∈ ω
60		f1of1 5585	. . . . . . . . . . . . 13 ⊢ (𝐺:ω–1-1-onto→ℕ0 → 𝐺:ω–1-1→ℕ0)
61	46, 60	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝐺:ω–1-1→ℕ0
62		f1fveq 5918	. . . . . . . . . . . 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 5924	. . . . . . . . . 10 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑓‘𝑥) ∈ ℕ0) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
68	46, 57, 67	sylancr 414	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
69	68	eqeq1d 2239	. . . . . . . 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 2525	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
72	71	dcbid 845	. . . . 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 2604	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
75		fveq1 5641	. . . . . . . . 9 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (𝑓‘𝑥) = ((𝐺 ∘ 𝑔)‘𝑥))
76	75	eqeq1d 2239	. . . . . . . 8 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 1 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 1))
77	76	ralbidv 2531	. . . . . . 7 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
78	77	dcbid 845	. . . . . 6 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ DECID ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
79		simplr 529	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
80	7	2o01f 16653	. . . . . . . 8 ⊢ (𝐺 ↾ 2o):2o⟶{0, 1}
81		elmapi 6844	. . . . . . . . 9 ⊢ (𝑔 ∈ (2o ↑𝑚 𝐴) → 𝑔:𝐴⟶2o)
82	81	adantl 277	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → 𝑔:𝐴⟶2o)
83		fco2 5503	. . . . . . . 8 ⊢ (((𝐺 ↾ 2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
84	80, 82, 83	sylancr 414	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
85		prexg 4303	. . . . . . . . . 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 6836	. . . . . . 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 2914	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → DECID ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1)
92		nfcv 2373	. . . . . . . . . 10 ⊢ Ⅎ𝑥({0, 1} ↑𝑚 𝐴)
93		nfra1 2562	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
94	93	nfdc 1706	. . . . . . . . . 10 ⊢ Ⅎ𝑥DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
95	92, 94	nfralxy 2569	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
96	20, 95	nfan 1613	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
97		nfv 1576	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑔 ∈ (2o ↑𝑚 𝐴)
98	96, 97	nfan 1613	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴))
99	81	ad2antlr 489	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶2o)
100		fvco3 5720	. . . . . . . . . 10 ⊢ ((𝑔:𝐴⟶2o ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
101	99, 100	sylancom 420	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
102	101	eqeq1d 2239	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔‘𝑥)) = 1))
103		f1of 5586	. . . . . . . . . . 11 ⊢ (𝐺:ω–1-1-onto→ℕ0 → 𝐺:ω⟶ℕ0)
104	46, 103	mp1i 10	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝐺:ω⟶ℕ0)
105		omelon 4709	. . . . . . . . . . . . . 14 ⊢ ω ∈ On
106	105	onelssi 4528	. . . . . . . . . . . . 13 ⊢ (2o ∈ ω → 2o ⊆ ω)
107	13, 106	mp1i 10	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 2o ⊆ ω)
108	99, 107	fssd 5497	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶ω)
109		simpr 110	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
110	108, 109	ffvelcdmd 5786	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ω)
111	104, 110	ffvelcdmd 5786	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(𝑔‘𝑥)) ∈ ℕ0)
112		f1ocnvfv 5925	. . . . . . . . . . . . 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 2241	. . . . . . . . . 10 ⊢ ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1) ↔ (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o)
116		f1of1 5585	. . . . . . . . . . . . 13 ⊢ (◡𝐺:ℕ0–1-1-onto→ω → ◡𝐺:ℕ0–1-1→ω)
117	46, 47, 116	mp2b 8	. . . . . . . . . . . 12 ⊢ ◡𝐺:ℕ0–1-1→ω
118		f1fveq 5918	. . . . . . . . . . . 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 5923	. . . . . . . . . 10 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑔‘𝑥) ∈ ω) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
124	46, 110, 123	sylancr 414	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
125	124	eqeq1d 2239	. . . . . . . 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 2525	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
128	127	dcbid 845	. . . . 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 2604	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
131	74, 130	impbida 600	. 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 841   = wceq 1397  ⊤wtru 1398   ∈ wcel 2201  ∀wral 2509  Vcvv 2801   ⊆ wss 3199  ∅c0 3493  {cpr 3671   ↦ cmpt 4151  suc csuc 4464  ωcom 4690  ^◡ccnv 4726   ↾ cres 4729   ∘ ccom 4731  ⟶wf 5324  –1-1→wf1 5325  –1-1-onto→wf1o 5327  ‘cfv 5328  (class class class)co 6023  freccfrec 6561  1_oc1o 6580  2_oc2o 6581   ↑_𝑚 cmap 6822  WOmnicwomni 7367  0cc0 8037  1c1 8038   + caddc 8040  ℕ₀cn0 9407  ℤcz 9484

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-coll 4205  ax-sep 4208  ax-nul 4216  ax-pow 4266  ax-pr 4301  ax-un 4532  ax-setind 4637  ax-iinf 4688  ax-cnex 8128  ax-resscn 8129  ax-1cn 8130  ax-1re 8131  ax-icn 8132  ax-addcl 8133  ax-addrcl 8134  ax-mulcl 8135  ax-addcom 8137  ax-addass 8139  ax-distr 8141  ax-i2m1 8142  ax-0lt1 8143  ax-0id 8145  ax-rnegex 8146  ax-cnre 8148  ax-pre-ltirr 8149  ax-pre-ltwlin 8150  ax-pre-lttrn 8151  ax-pre-ltadd 8153

This theorem depends on definitions:  df-bi 117  df-dc 842  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-nel 2497  df-ral 2514  df-rex 2515  df-reu 2516  df-rab 2518  df-v 2803  df-sbc 3031  df-csb 3127  df-dif 3201  df-un 3203  df-in 3205  df-ss 3212  df-nul 3494  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-int 3930  df-iun 3973  df-br 4090  df-opab 4152  df-mpt 4153  df-tr 4189  df-id 4392  df-iord 4465  df-on 4467  df-ilim 4468  df-suc 4470  df-iom 4691  df-xp 4733  df-rel 4734  df-cnv 4735  df-co 4736  df-dm 4737  df-rn 4738  df-res 4739  df-ima 4740  df-iota 5288  df-fun 5330  df-fn 5331  df-f 5332  df-f1 5333  df-fo 5334  df-f1o 5335  df-fv 5336  df-riota 5976  df-ov 6026  df-oprab 6027  df-mpo 6028  df-recs 6476  df-frec 6562  df-1o 6587  df-2o 6588  df-map 6824  df-womni 7368  df-pnf 8221  df-mnf 8222  df-xr 8223  df-ltxr 8224  df-le 8225  df-sub 8357  df-neg 8358  df-inn 9149  df-n0 9408  df-z 9485  df-uz 9761

This theorem is referenced by:  iswomninn  16722