Theorem iswomninnlem 16062

Description: Lemma for iswomnimap 7275. 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 7275	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
2		fveq1 5582	. . . . . . . . 9 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (𝑔‘𝑥) = ((◡𝐺 ∘ 𝑓)‘𝑥))
3	2	eqeq1d 2215	. . . . . . . 8 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = 1o ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
4	3	ralbidv 2507	. . . . . . 7 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
5	4	dcbid 840	. . . . . 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 16004	. . . . . . . . . 10 ⊢ (◡𝐺 ↾ {0, 1}):{0, 1}⟶2o
9		elmapi 6764	. . . . . . . . . 10 ⊢ (𝑓 ∈ ({0, 1} ↑𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
10		fco2 5448	. . . . . . . . . 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 6614	. . . . . . . . . 10 ⊢ 2o ∈ ω
14	13	a1i 9	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 2o ∈ ω)
15		simpl 109	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝐴 ∈ 𝑉)
16	14, 15	elmapd 6756	. . . . . . . 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 2883	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → DECID ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)
20		nfv 1552	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑉
21		nfcv 2349	. . . . . . . . . 10 ⊢ Ⅎ𝑥(2o ↑𝑚 𝐴)
22		nfra1 2538	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
23	22	nfdc 1683	. . . . . . . . . 10 ⊢ Ⅎ𝑥DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
24	21, 23	nfralxy 2545	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
25	20, 24	nfan 1589	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
26		nfv 1552	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)
27	25, 26	nfan 1589	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴))
28	9	ad2antlr 489	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1})
29		fvco3 5657	. . . . . . . . . 10 ⊢ ((𝑓:𝐴⟶{0, 1} ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
30	28, 29	sylancom 420	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
31	30	eqeq1d 2215	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o))
32		df-1o 6509	. . . . . . . . . . . 12 ⊢ 1o = suc ∅
33	32	fveq2i 5586	. . . . . . . . . . 11 ⊢ (𝐺‘1o) = (𝐺‘suc ∅)
34		0zd 9391	. . . . . . . . . . . . 13 ⊢ (⊤ → 0 ∈ ℤ)
35		peano1 4646	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ ω
36	35	a1i 9	. . . . . . . . . . . . 13 ⊢ (⊤ → ∅ ∈ ω)
37	34, 7, 36	frec2uzsucd 10553	. . . . . . . . . . . 12 ⊢ (⊤ → (𝐺‘suc ∅) = ((𝐺‘∅) + 1))
38	37	mptru 1382	. . . . . . . . . . 11 ⊢ (𝐺‘suc ∅) = ((𝐺‘∅) + 1)
39	34, 7	frec2uz0d 10551	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝐺‘∅) = 0)
40	39	mptru 1382	. . . . . . . . . . . . 13 ⊢ (𝐺‘∅) = 0
41	40	oveq1i 5961	. . . . . . . . . . . 12 ⊢ ((𝐺‘∅) + 1) = (0 + 1)
42		0p1e1 9157	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
43	41, 42	eqtri 2227	. . . . . . . . . . 11 ⊢ ((𝐺‘∅) + 1) = 1
44	33, 38, 43	3eqtri 2231	. . . . . . . . . 10 ⊢ (𝐺‘1o) = 1
45	44	eqeq2i 2217	. . . . . . . . 9 ⊢ ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1)
46	7	frechashgf1o 10580	. . . . . . . . . . . . 13 ⊢ 𝐺:ω–1-1-onto→ℕ0
47		f1ocnv 5542	. . . . . . . . . . . . 13 ⊢ (𝐺:ω–1-1-onto→ℕ0 → ◡𝐺:ℕ0–1-1-onto→ω)
48		f1of 5529	. . . . . . . . . . . . 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 9317	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
52		1nn0 9318	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ0
53		prssi 3793	. . . . . . . . . . . . 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 5723	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1})
57	54, 56	sselid 3192	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℕ0)
58	50, 57	ffvelcdmd 5723	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝑓‘𝑥)) ∈ ω)
59		1onn 6613	. . . . . . . . . . 11 ⊢ 1o ∈ ω
60		f1of1 5528	. . . . . . . . . . . . 13 ⊢ (𝐺:ω–1-1-onto→ℕ0 → 𝐺:ω–1-1→ℕ0)
61	46, 60	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝐺:ω–1-1→ℕ0
62		f1fveq 5848	. . . . . . . . . . . 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 5854	. . . . . . . . . 10 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑓‘𝑥) ∈ ℕ0) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
68	46, 57, 67	sylancr 414	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
69	68	eqeq1d 2215	. . . . . . . 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 2501	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
72	71	dcbid 840	. . . . 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 2580	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
75		fveq1 5582	. . . . . . . . 9 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (𝑓‘𝑥) = ((𝐺 ∘ 𝑔)‘𝑥))
76	75	eqeq1d 2215	. . . . . . . 8 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 1 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 1))
77	76	ralbidv 2507	. . . . . . 7 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
78	77	dcbid 840	. . . . . 6 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ DECID ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
79		simplr 528	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
80	7	2o01f 16005	. . . . . . . 8 ⊢ (𝐺 ↾ 2o):2o⟶{0, 1}
81		elmapi 6764	. . . . . . . . 9 ⊢ (𝑔 ∈ (2o ↑𝑚 𝐴) → 𝑔:𝐴⟶2o)
82	81	adantl 277	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → 𝑔:𝐴⟶2o)
83		fco2 5448	. . . . . . . 8 ⊢ (((𝐺 ↾ 2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
84	80, 82, 83	sylancr 414	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
85		prexg 4259	. . . . . . . . . 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 6756	. . . . . . 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 2883	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → DECID ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1)
92		nfcv 2349	. . . . . . . . . 10 ⊢ Ⅎ𝑥({0, 1} ↑𝑚 𝐴)
93		nfra1 2538	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
94	93	nfdc 1683	. . . . . . . . . 10 ⊢ Ⅎ𝑥DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
95	92, 94	nfralxy 2545	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
96	20, 95	nfan 1589	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
97		nfv 1552	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑔 ∈ (2o ↑𝑚 𝐴)
98	96, 97	nfan 1589	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴))
99	81	ad2antlr 489	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶2o)
100		fvco3 5657	. . . . . . . . . 10 ⊢ ((𝑔:𝐴⟶2o ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
101	99, 100	sylancom 420	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
102	101	eqeq1d 2215	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔‘𝑥)) = 1))
103		f1of 5529	. . . . . . . . . . 11 ⊢ (𝐺:ω–1-1-onto→ℕ0 → 𝐺:ω⟶ℕ0)
104	46, 103	mp1i 10	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝐺:ω⟶ℕ0)
105		omelon 4661	. . . . . . . . . . . . . 14 ⊢ ω ∈ On
106	105	onelssi 4480	. . . . . . . . . . . . 13 ⊢ (2o ∈ ω → 2o ⊆ ω)
107	13, 106	mp1i 10	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 2o ⊆ ω)
108	99, 107	fssd 5444	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶ω)
109		simpr 110	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
110	108, 109	ffvelcdmd 5723	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ω)
111	104, 110	ffvelcdmd 5723	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(𝑔‘𝑥)) ∈ ℕ0)
112		f1ocnvfv 5855	. . . . . . . . . . . . 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 2217	. . . . . . . . . 10 ⊢ ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1) ↔ (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o)
116		f1of1 5528	. . . . . . . . . . . . 13 ⊢ (◡𝐺:ℕ0–1-1-onto→ω → ◡𝐺:ℕ0–1-1→ω)
117	46, 47, 116	mp2b 8	. . . . . . . . . . . 12 ⊢ ◡𝐺:ℕ0–1-1→ω
118		f1fveq 5848	. . . . . . . . . . . 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 5853	. . . . . . . . . 10 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑔‘𝑥) ∈ ω) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
124	46, 110, 123	sylancr 414	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
125	124	eqeq1d 2215	. . . . . . . 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 2501	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
128	127	dcbid 840	. . . . 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 2580	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
131	74, 130	impbida 596	. 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 836   = wceq 1373  ⊤wtru 1374   ∈ wcel 2177  ∀wral 2485  Vcvv 2773   ⊆ wss 3167  ∅c0 3461  {cpr 3635   ↦ cmpt 4109  suc csuc 4416  ωcom 4642  ^◡ccnv 4678   ↾ cres 4681   ∘ ccom 4683  ⟶wf 5272  –1-1→wf1 5273  –1-1-onto→wf1o 5275  ‘cfv 5276  (class class class)co 5951  freccfrec 6483  1_oc1o 6502  2_oc2o 6503   ↑_𝑚 cmap 6742  WOmnicwomni 7272  0cc0 7932  1c1 7933   + caddc 7935  ℕ₀cn0 9302  ℤcz 9379

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 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-coll 4163  ax-sep 4166  ax-nul 4174  ax-pow 4222  ax-pr 4257  ax-un 4484  ax-setind 4589  ax-iinf 4640  ax-cnex 8023  ax-resscn 8024  ax-1cn 8025  ax-1re 8026  ax-icn 8027  ax-addcl 8028  ax-addrcl 8029  ax-mulcl 8030  ax-addcom 8032  ax-addass 8034  ax-distr 8036  ax-i2m1 8037  ax-0lt1 8038  ax-0id 8040  ax-rnegex 8041  ax-cnre 8043  ax-pre-ltirr 8044  ax-pre-ltwlin 8045  ax-pre-lttrn 8046  ax-pre-ltadd 8048

This theorem depends on definitions:  df-bi 117  df-dc 837  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-nel 2473  df-ral 2490  df-rex 2491  df-reu 2492  df-rab 2494  df-v 2775  df-sbc 3000  df-csb 3095  df-dif 3169  df-un 3171  df-in 3173  df-ss 3180  df-nul 3462  df-pw 3619  df-sn 3640  df-pr 3641  df-op 3643  df-uni 3853  df-int 3888  df-iun 3931  df-br 4048  df-opab 4110  df-mpt 4111  df-tr 4147  df-id 4344  df-iord 4417  df-on 4419  df-ilim 4420  df-suc 4422  df-iom 4643  df-xp 4685  df-rel 4686  df-cnv 4687  df-co 4688  df-dm 4689  df-rn 4690  df-res 4691  df-ima 4692  df-iota 5237  df-fun 5278  df-fn 5279  df-f 5280  df-f1 5281  df-fo 5282  df-f1o 5283  df-fv 5284  df-riota 5906  df-ov 5954  df-oprab 5955  df-mpo 5956  df-recs 6398  df-frec 6484  df-1o 6509  df-2o 6510  df-map 6744  df-womni 7273  df-pnf 8116  df-mnf 8117  df-xr 8118  df-ltxr 8119  df-le 8120  df-sub 8252  df-neg 8253  df-inn 9044  df-n0 9303  df-z 9380  df-uz 9656

This theorem is referenced by:  iswomninn  16063