Theorem iswomninnlem 13561

Description: Lemma for iswomnimap 7088. 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 7088	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
2		fveq1 5460	. . . . . . . . 9 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (𝑔‘𝑥) = ((◡𝐺 ∘ 𝑓)‘𝑥))
3	2	eqeq1d 2163	. . . . . . . 8 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = 1o ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
4	3	ralbidv 2454	. . . . . . 7 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
5	4	dcbid 824	. . . . . 6 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ DECID ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
6		simplr 520	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
7		iswomninnlem.g	. . . . . . . . . . 11 ⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
8	7	012of 13506	. . . . . . . . . 10 ⊢ (◡𝐺 ↾ {0, 1}):{0, 1}⟶2o
9		elmapi 6604	. . . . . . . . . 10 ⊢ (𝑓 ∈ ({0, 1} ↑𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
10		fco2 5329	. . . . . . . . . 10 ⊢ (((◡𝐺 ↾ {0, 1}):{0, 1}⟶2o ∧ 𝑓:𝐴⟶{0, 1}) → (◡𝐺 ∘ 𝑓):𝐴⟶2o)
11	8, 9, 10	sylancr 411	. . . . . . . . 9 ⊢ (𝑓 ∈ ({0, 1} ↑𝑚 𝐴) → (◡𝐺 ∘ 𝑓):𝐴⟶2o)
12	11	adantl 275	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (◡𝐺 ∘ 𝑓):𝐴⟶2o)
13		2onn 6457	. . . . . . . . . 10 ⊢ 2o ∈ ω
14	13	a1i 9	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 2o ∈ ω)
15		simpl 108	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝐴 ∈ 𝑉)
16	14, 15	elmapd 6596	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ((◡𝐺 ∘ 𝑓) ∈ (2o ↑𝑚 𝐴) ↔ (◡𝐺 ∘ 𝑓):𝐴⟶2o))
17	12, 16	mpbird 166	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (◡𝐺 ∘ 𝑓) ∈ (2o ↑𝑚 𝐴))
18	17	adantlr 469	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (◡𝐺 ∘ 𝑓) ∈ (2o ↑𝑚 𝐴))
19	5, 6, 18	rspcdva 2818	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → DECID ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)
20		nfv 1505	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑉
21		nfcv 2296	. . . . . . . . . 10 ⊢ Ⅎ𝑥(2o ↑𝑚 𝐴)
22		nfra1 2485	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
23	22	nfdc 1636	. . . . . . . . . 10 ⊢ Ⅎ𝑥DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
24	21, 23	nfralxy 2492	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
25	20, 24	nfan 1542	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
26		nfv 1505	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)
27	25, 26	nfan 1542	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴))
28	9	ad2antlr 481	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1})
29		fvco3 5532	. . . . . . . . . 10 ⊢ ((𝑓:𝐴⟶{0, 1} ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
30	28, 29	sylancom 417	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
31	30	eqeq1d 2163	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o))
32		df-1o 6353	. . . . . . . . . . . 12 ⊢ 1o = suc ∅
33	32	fveq2i 5464	. . . . . . . . . . 11 ⊢ (𝐺‘1o) = (𝐺‘suc ∅)
34		0zd 9158	. . . . . . . . . . . . 13 ⊢ (⊤ → 0 ∈ ℤ)
35		peano1 4547	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ ω
36	35	a1i 9	. . . . . . . . . . . . 13 ⊢ (⊤ → ∅ ∈ ω)
37	34, 7, 36	frec2uzsucd 10278	. . . . . . . . . . . 12 ⊢ (⊤ → (𝐺‘suc ∅) = ((𝐺‘∅) + 1))
38	37	mptru 1341	. . . . . . . . . . 11 ⊢ (𝐺‘suc ∅) = ((𝐺‘∅) + 1)
39	34, 7	frec2uz0d 10276	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝐺‘∅) = 0)
40	39	mptru 1341	. . . . . . . . . . . . 13 ⊢ (𝐺‘∅) = 0
41	40	oveq1i 5824	. . . . . . . . . . . 12 ⊢ ((𝐺‘∅) + 1) = (0 + 1)
42		0p1e1 8926	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
43	41, 42	eqtri 2175	. . . . . . . . . . 11 ⊢ ((𝐺‘∅) + 1) = 1
44	33, 38, 43	3eqtri 2179	. . . . . . . . . 10 ⊢ (𝐺‘1o) = 1
45	44	eqeq2i 2165	. . . . . . . . 9 ⊢ ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1)
46	7	frechashgf1o 10305	. . . . . . . . . . . . 13 ⊢ 𝐺:ω–1-1-onto→ℕ0
47		f1ocnv 5420	. . . . . . . . . . . . 13 ⊢ (𝐺:ω–1-1-onto→ℕ0 → ◡𝐺:ℕ0–1-1-onto→ω)
48		f1of 5407	. . . . . . . . . . . . 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 9084	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
52		1nn0 9085	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ0
53		prssi 3710	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
54	51, 52, 53	mp2an 423	. . . . . . . . . . . 12 ⊢ {0, 1} ⊆ ℕ0
55		simpr 109	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
56	28, 55	ffvelrnd 5596	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1})
57	54, 56	sseldi 3122	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℕ0)
58	50, 57	ffvelrnd 5596	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝑓‘𝑥)) ∈ ω)
59		1onn 6456	. . . . . . . . . . 11 ⊢ 1o ∈ ω
60		f1of1 5406	. . . . . . . . . . . . 13 ⊢ (𝐺:ω–1-1-onto→ℕ0 → 𝐺:ω–1-1→ℕ0)
61	46, 60	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝐺:ω–1-1→ℕ0
62		f1fveq 5713	. . . . . . . . . . . 12 ⊢ ((𝐺:ω–1-1→ℕ0 ∧ ((◡𝐺‘(𝑓‘𝑥)) ∈ ω ∧ 1o ∈ ω)) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o))
63	61, 62	mpan 421	. . . . . . . . . . 11 ⊢ (((◡𝐺‘(𝑓‘𝑥)) ∈ ω ∧ 1o ∈ ω) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o))
64	59, 63	mpan2 422	. . . . . . . . . 10 ⊢ ((◡𝐺‘(𝑓‘𝑥)) ∈ ω → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o))
65	58, 64	syl 14	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o))
66	45, 65	bitr3id 193	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1 ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o))
67		f1ocnvfv2 5719	. . . . . . . . . 10 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑓‘𝑥) ∈ ℕ0) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
68	46, 57, 67	sylancr 411	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
69	68	eqeq1d 2163	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1 ↔ (𝑓‘𝑥) = 1))
70	31, 66, 69	3bitr2d 215	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ (𝑓‘𝑥) = 1))
71	27, 70	ralbida 2448	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
72	71	dcbid 824	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (DECID ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
73	19, 72	mpbid 146	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
74	73	ralrimiva 2527	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
75		fveq1 5460	. . . . . . . . 9 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (𝑓‘𝑥) = ((𝐺 ∘ 𝑔)‘𝑥))
76	75	eqeq1d 2163	. . . . . . . 8 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 1 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 1))
77	76	ralbidv 2454	. . . . . . 7 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
78	77	dcbid 824	. . . . . 6 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ DECID ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
79		simplr 520	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
80	7	2o01f 13507	. . . . . . . 8 ⊢ (𝐺 ↾ 2o):2o⟶{0, 1}
81		elmapi 6604	. . . . . . . . 9 ⊢ (𝑔 ∈ (2o ↑𝑚 𝐴) → 𝑔:𝐴⟶2o)
82	81	adantl 275	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → 𝑔:𝐴⟶2o)
83		fco2 5329	. . . . . . . 8 ⊢ (((𝐺 ↾ 2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
84	80, 82, 83	sylancr 411	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
85		prexg 4166	. . . . . . . . . 10 ⊢ ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ∈ V)
86	51, 52, 85	mp2an 423	. . . . . . . . 9 ⊢ {0, 1} ∈ V
87	86	a1i 9	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → {0, 1} ∈ V)
88		simpll 519	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → 𝐴 ∈ 𝑉)
89	87, 88	elmapd 6596	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → ((𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚 𝐴) ↔ (𝐺 ∘ 𝑔):𝐴⟶{0, 1}))
90	84, 89	mpbird 166	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚 𝐴))
91	78, 79, 90	rspcdva 2818	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → DECID ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1)
92		nfcv 2296	. . . . . . . . . 10 ⊢ Ⅎ𝑥({0, 1} ↑𝑚 𝐴)
93		nfra1 2485	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
94	93	nfdc 1636	. . . . . . . . . 10 ⊢ Ⅎ𝑥DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
95	92, 94	nfralxy 2492	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
96	20, 95	nfan 1542	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
97		nfv 1505	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑔 ∈ (2o ↑𝑚 𝐴)
98	96, 97	nfan 1542	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴))
99	81	ad2antlr 481	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶2o)
100		fvco3 5532	. . . . . . . . . 10 ⊢ ((𝑔:𝐴⟶2o ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
101	99, 100	sylancom 417	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
102	101	eqeq1d 2163	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔‘𝑥)) = 1))
103		f1of 5407	. . . . . . . . . . 11 ⊢ (𝐺:ω–1-1-onto→ℕ0 → 𝐺:ω⟶ℕ0)
104	46, 103	mp1i 10	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝐺:ω⟶ℕ0)
105		omelon 4562	. . . . . . . . . . . . . 14 ⊢ ω ∈ On
106	105	onelssi 4384	. . . . . . . . . . . . 13 ⊢ (2o ∈ ω → 2o ⊆ ω)
107	13, 106	mp1i 10	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 2o ⊆ ω)
108	99, 107	fssd 5325	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶ω)
109		simpr 109	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
110	108, 109	ffvelrnd 5596	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ω)
111	104, 110	ffvelrnd 5596	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(𝑔‘𝑥)) ∈ ℕ0)
112		f1ocnvfv 5720	. . . . . . . . . . . . 13 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ 1o ∈ ω) → ((𝐺‘1o) = 1 → (◡𝐺‘1) = 1o))
113	46, 59, 112	mp2an 423	. . . . . . . . . . . 12 ⊢ ((𝐺‘1o) = 1 → (◡𝐺‘1) = 1o)
114	44, 113	ax-mp 5	. . . . . . . . . . 11 ⊢ (◡𝐺‘1) = 1o
115	114	eqeq2i 2165	. . . . . . . . . 10 ⊢ ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1) ↔ (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o)
116		f1of1 5406	. . . . . . . . . . . . 13 ⊢ (◡𝐺:ℕ0–1-1-onto→ω → ◡𝐺:ℕ0–1-1→ω)
117	46, 47, 116	mp2b 8	. . . . . . . . . . . 12 ⊢ ◡𝐺:ℕ0–1-1→ω
118		f1fveq 5713	. . . . . . . . . . . 12 ⊢ ((◡𝐺:ℕ0–1-1→ω ∧ ((𝐺‘(𝑔‘𝑥)) ∈ ℕ0 ∧ 1 ∈ ℕ0)) → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1) ↔ (𝐺‘(𝑔‘𝑥)) = 1))
119	117, 118	mpan 421	. . . . . . . . . . 11 ⊢ (((𝐺‘(𝑔‘𝑥)) ∈ ℕ0 ∧ 1 ∈ ℕ0) → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1) ↔ (𝐺‘(𝑔‘𝑥)) = 1))
120	52, 119	mpan2 422	. . . . . . . . . 10 ⊢ ((𝐺‘(𝑔‘𝑥)) ∈ ℕ0 → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1) ↔ (𝐺‘(𝑔‘𝑥)) = 1))
121	115, 120	bitr3id 193	. . . . . . . . 9 ⊢ ((𝐺‘(𝑔‘𝑥)) ∈ ℕ0 → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o ↔ (𝐺‘(𝑔‘𝑥)) = 1))
122	111, 121	syl 14	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o ↔ (𝐺‘(𝑔‘𝑥)) = 1))
123		f1ocnvfv1 5718	. . . . . . . . . 10 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑔‘𝑥) ∈ ω) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
124	46, 110, 123	sylancr 411	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
125	124	eqeq1d 2163	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o ↔ (𝑔‘𝑥) = 1o))
126	102, 122, 125	3bitr2d 215	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ (𝑔‘𝑥) = 1o))
127	98, 126	ralbida 2448	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
128	127	dcbid 824	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (DECID ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
129	91, 128	mpbid 146	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
130	129	ralrimiva 2527	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
131	74, 130	impbida 586	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
132	1, 131	bitrd 187	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  DECID wdc 820   = wceq 1332  ⊤wtru 1333   ∈ wcel 2125  ∀wral 2432  Vcvv 2709   ⊆ wss 3098  ∅c0 3390  {cpr 3557   ↦ cmpt 4021  suc csuc 4320  ωcom 4543  ^◡ccnv 4578   ↾ cres 4581   ∘ ccom 4583  ⟶wf 5159  –1-1→wf1 5160  –1-1-onto→wf1o 5162  ‘cfv 5163  (class class class)co 5814  freccfrec 6327  1_oc1o 6346  2_oc2o 6347   ↑_𝑚 cmap 6582  WOmnicwomni 7085  0cc0 7711  1c1 7712   + caddc 7714  ℕ₀cn0 9069  ℤcz 9146

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-coll 4075  ax-sep 4078  ax-nul 4086  ax-pow 4130  ax-pr 4164  ax-un 4388  ax-setind 4490  ax-iinf 4541  ax-cnex 7802  ax-resscn 7803  ax-1cn 7804  ax-1re 7805  ax-icn 7806  ax-addcl 7807  ax-addrcl 7808  ax-mulcl 7809  ax-addcom 7811  ax-addass 7813  ax-distr 7815  ax-i2m1 7816  ax-0lt1 7817  ax-0id 7819  ax-rnegex 7820  ax-cnre 7822  ax-pre-ltirr 7823  ax-pre-ltwlin 7824  ax-pre-lttrn 7825  ax-pre-ltadd 7827

This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  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-nel 2420  df-ral 2437  df-rex 2438  df-reu 2439  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-iun 3847  df-br 3962  df-opab 4022  df-mpt 4023  df-tr 4059  df-id 4248  df-iord 4321  df-on 4323  df-ilim 4324  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-f1 5168  df-fo 5169  df-f1o 5170  df-fv 5171  df-riota 5770  df-ov 5817  df-oprab 5818  df-mpo 5819  df-recs 6242  df-frec 6328  df-1o 6353  df-2o 6354  df-map 6584  df-womni 7086  df-pnf 7893  df-mnf 7894  df-xr 7895  df-ltxr 7896  df-le 7897  df-sub 8027  df-neg 8028  df-inn 8813  df-n0 9070  df-z 9147  df-uz 9419

This theorem is referenced by:  iswomninn  13562