Theorem isomninnlem 13225

Description: Lemma for isomninn 13226. 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.

Step	Hyp	Ref	Expression
1		isomnimap 7009	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)))
2		fveq1 5420	. . . . . . . . 9 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (𝑔‘𝑥) = ((◡𝐺 ∘ 𝑓)‘𝑥))
3	2	eqeq1d 2148	. . . . . . . 8 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = ∅ ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅))
4	3	rexbidv 2438	. . . . . . 7 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅))
5	2	eqeq1d 2148	. . . . . . . 8 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = 1o ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
6	5	ralbidv 2437	. . . . . . 7 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
7	4, 6	orbi12d 782	. . . . . 6 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ↔ (∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)))
8		simplr 519	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
9		isomninnlem.g	. . . . . . . . . . . . 13 ⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
10	9	frechashgf1o 10201	. . . . . . . . . . . 12 ⊢ 𝐺:ω–1-1-onto→ℕ0
11		f1ocnv 5380	. . . . . . . . . . . 12 ⊢ (𝐺:ω–1-1-onto→ℕ0 → ◡𝐺:ℕ0–1-1-onto→ω)
12		f1of 5367	. . . . . . . . . . . 12 ⊢ (◡𝐺:ℕ0–1-1-onto→ω → ◡𝐺:ℕ0⟶ω)
13	10, 11, 12	mp2b 8	. . . . . . . . . . 11 ⊢ ◡𝐺:ℕ0⟶ω
14		0nn0 8992	. . . . . . . . . . . 12 ⊢ 0 ∈ ℕ0
15		1nn0 8993	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ0
16		prssi 3678	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
17	14, 15, 16	mp2an 422	. . . . . . . . . . 11 ⊢ {0, 1} ⊆ ℕ0
18		fssres 5298	. . . . . . . . . . 11 ⊢ ((◡𝐺:ℕ0⟶ω ∧ {0, 1} ⊆ ℕ0) → (◡𝐺 ↾ {0, 1}):{0, 1}⟶ω)
19	13, 17, 18	mp2an 422	. . . . . . . . . 10 ⊢ (◡𝐺 ↾ {0, 1}):{0, 1}⟶ω
20		ffn 5272	. . . . . . . . . 10 ⊢ ((◡𝐺 ↾ {0, 1}):{0, 1}⟶ω → (◡𝐺 ↾ {0, 1}) Fn {0, 1})
21	19, 20	ax-mp 5	. . . . . . . . 9 ⊢ (◡𝐺 ↾ {0, 1}) Fn {0, 1}
22		fvres 5445	. . . . . . . . . . 11 ⊢ (𝑗 ∈ {0, 1} → ((◡𝐺 ↾ {0, 1})‘𝑗) = (◡𝐺‘𝑗))
23		elpri 3550	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ {0, 1} → (𝑗 = 0 ∨ 𝑗 = 1))
24		fveq2 5421	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 0 → (◡𝐺‘𝑗) = (◡𝐺‘0))
25		0zd 9066	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → 0 ∈ ℤ)
26	25, 9	frec2uz0d 10172	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (𝐺‘∅) = 0)
27	26	mptru 1340	. . . . . . . . . . . . . . . 16 ⊢ (𝐺‘∅) = 0
28		peano1 4508	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ ω
29		f1ocnvfv 5680	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ ∅ ∈ ω) → ((𝐺‘∅) = 0 → (◡𝐺‘0) = ∅))
30	10, 28, 29	mp2an 422	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘∅) = 0 → (◡𝐺‘0) = ∅)
31	27, 30	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (◡𝐺‘0) = ∅
32		0lt2o 6338	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ 2o
33	31, 32	eqeltri 2212	. . . . . . . . . . . . . 14 ⊢ (◡𝐺‘0) ∈ 2o
34	24, 33	eqeltrdi 2230	. . . . . . . . . . . . 13 ⊢ (𝑗 = 0 → (◡𝐺‘𝑗) ∈ 2o)
35		fveq2 5421	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 1 → (◡𝐺‘𝑗) = (◡𝐺‘1))
36		df-1o 6313	. . . . . . . . . . . . . . . . . 18 ⊢ 1o = suc ∅
37	36	fveq2i 5424	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺‘1o) = (𝐺‘suc ∅)
38	28	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ∅ ∈ ω)
39	25, 9, 38	frec2uzsucd 10174	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (𝐺‘suc ∅) = ((𝐺‘∅) + 1))
40	39	mptru 1340	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺‘suc ∅) = ((𝐺‘∅) + 1)
41	27	oveq1i 5784	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘∅) + 1) = (0 + 1)
42		0p1e1 8834	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + 1) = 1
43	41, 42	eqtri 2160	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘∅) + 1) = 1
44	37, 40, 43	3eqtri 2164	. . . . . . . . . . . . . . . 16 ⊢ (𝐺‘1o) = 1
45		1onn 6416	. . . . . . . . . . . . . . . . 17 ⊢ 1o ∈ ω
46		f1ocnvfv 5680	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ 1o ∈ ω) → ((𝐺‘1o) = 1 → (◡𝐺‘1) = 1o))
47	10, 45, 46	mp2an 422	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘1o) = 1 → (◡𝐺‘1) = 1o)
48	44, 47	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (◡𝐺‘1) = 1o
49		1lt2o 6339	. . . . . . . . . . . . . . 15 ⊢ 1o ∈ 2o
50	48, 49	eqeltri 2212	. . . . . . . . . . . . . 14 ⊢ (◡𝐺‘1) ∈ 2o
51	35, 50	eqeltrdi 2230	. . . . . . . . . . . . 13 ⊢ (𝑗 = 1 → (◡𝐺‘𝑗) ∈ 2o)
52	34, 51	jaoi 705	. . . . . . . . . . . 12 ⊢ ((𝑗 = 0 ∨ 𝑗 = 1) → (◡𝐺‘𝑗) ∈ 2o)
53	23, 52	syl 14	. . . . . . . . . . 11 ⊢ (𝑗 ∈ {0, 1} → (◡𝐺‘𝑗) ∈ 2o)
54	22, 53	eqeltrd 2216	. . . . . . . . . 10 ⊢ (𝑗 ∈ {0, 1} → ((◡𝐺 ↾ {0, 1})‘𝑗) ∈ 2o)
55	54	rgen 2485	. . . . . . . . 9 ⊢ ∀𝑗 ∈ {0, 1} ((◡𝐺 ↾ {0, 1})‘𝑗) ∈ 2o
56		ffnfv 5578	. . . . . . . . 9 ⊢ ((◡𝐺 ↾ {0, 1}):{0, 1}⟶2o ↔ ((◡𝐺 ↾ {0, 1}) Fn {0, 1} ∧ ∀𝑗 ∈ {0, 1} ((◡𝐺 ↾ {0, 1})‘𝑗) ∈ 2o))
57	21, 55, 56	mpbir2an 926	. . . . . . . 8 ⊢ (◡𝐺 ↾ {0, 1}):{0, 1}⟶2o
58		elmapi 6564	. . . . . . . . 9 ⊢ (𝑓 ∈ ({0, 1} ↑𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
59	58	adantl 275	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝑓:𝐴⟶{0, 1})
60		fco2 5289	. . . . . . . 8 ⊢ (((◡𝐺 ↾ {0, 1}):{0, 1}⟶2o ∧ 𝑓:𝐴⟶{0, 1}) → (◡𝐺 ∘ 𝑓):𝐴⟶2o)
61	57, 59, 60	sylancr 410	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (◡𝐺 ∘ 𝑓):𝐴⟶2o)
62		2onn 6417	. . . . . . . . 9 ⊢ 2o ∈ ω
63	62	a1i 9	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 2o ∈ ω)
64		simpll 518	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝐴 ∈ 𝑉)
65	63, 64	elmapd 6556	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ((◡𝐺 ∘ 𝑓) ∈ (2o ↑𝑚 𝐴) ↔ (◡𝐺 ∘ 𝑓):𝐴⟶2o))
66	61, 65	mpbird 166	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (◡𝐺 ∘ 𝑓) ∈ (2o ↑𝑚 𝐴))
67	7, 8, 66	rspcdva 2794	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
68		nfv 1508	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑉
69		nfcv 2281	. . . . . . . . . 10 ⊢ Ⅎ𝑥(2o ↑𝑚 𝐴)
70		nfre1 2476	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅
71		nfra1 2466	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
72	70, 71	nfor 1553	. . . . . . . . . 10 ⊢ Ⅎ𝑥(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
73	69, 72	nfralxy 2471	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)
74	68, 73	nfan 1544	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
75		nfv 1508	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)
76	74, 75	nfan 1544	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴))
77		simplr 519	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑓 ∈ ({0, 1} ↑𝑚 𝐴))
78	77, 58	syl 14	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1})
79		simpr 109	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
80	78, 79	ffvelrnd 5556	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1})
81	17, 80	sseldi 3095	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℕ0)
82		f1ocnvfv2 5679	. . . . . . . . . . 11 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑓‘𝑥) ∈ ℕ0) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
83	10, 81, 82	sylancr 410	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
84	83	adantr 274	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
85		fvco3 5492	. . . . . . . . . . . . . 14 ⊢ ((𝑓:𝐴⟶{0, 1} ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
86	78, 85	sylancom 416	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
87	86	eqeq1d 2148	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ ↔ (◡𝐺‘(𝑓‘𝑥)) = ∅))
88	87	biimpa 294	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (◡𝐺‘(𝑓‘𝑥)) = ∅)
89	88	fveq2d 5425	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘∅))
90	89, 27	syl6eq 2188	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 0)
91	84, 90	eqtr3d 2174	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝑓‘𝑥) = 0)
92	91	exp31 361	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝑥 ∈ 𝐴 → (((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ → (𝑓‘𝑥) = 0)))
93	76, 92	reximdai 2530	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
94	83	adantr 274	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
95	86	adantr 274	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
96		simpr 109	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)
97	95, 96	eqtr3d 2174	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (◡𝐺‘(𝑓‘𝑥)) = 1o)
98	97	fveq2d 5425	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o))
99	98, 44	syl6eq 2188	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1)
100	94, 99	eqtr3d 2174	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝑓‘𝑥) = 1)
101	100	ex 114	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → (𝑓‘𝑥) = 1))
102	76, 101	ralimdaa 2498	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
103	93, 102	orim12d 775	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ((∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)))
104	67, 103	mpd 13	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
105	104	ralrimiva 2505	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
106		fveq1 5420	. . . . . . . . 9 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (𝑓‘𝑥) = ((𝐺 ∘ 𝑔)‘𝑥))
107	106	eqeq1d 2148	. . . . . . . 8 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 0 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 0))
108	107	rexbidv 2438	. . . . . . 7 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ↔ ∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0))
109	106	eqeq1d 2148	. . . . . . . 8 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 1 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 1))
110	109	ralbidv 2437	. . . . . . 7 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
111	108, 110	orbi12d 782	. . . . . 6 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ↔ (∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1)))
112		simplr 519	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
113		f1of 5367	. . . . . . . . . . . 12 ⊢ (𝐺:ω–1-1-onto→ℕ0 → 𝐺:ω⟶ℕ0)
114	10, 113	ax-mp 5	. . . . . . . . . . 11 ⊢ 𝐺:ω⟶ℕ0
115		omelon 4522	. . . . . . . . . . . . 13 ⊢ ω ∈ On
116	115	onelssi 4351	. . . . . . . . . . . 12 ⊢ (2o ∈ ω → 2o ⊆ ω)
117	62, 116	ax-mp 5	. . . . . . . . . . 11 ⊢ 2o ⊆ ω
118		fssres 5298	. . . . . . . . . . 11 ⊢ ((𝐺:ω⟶ℕ0 ∧ 2o ⊆ ω) → (𝐺 ↾ 2o):2o⟶ℕ0)
119	114, 117, 118	mp2an 422	. . . . . . . . . 10 ⊢ (𝐺 ↾ 2o):2o⟶ℕ0
120		ffn 5272	. . . . . . . . . 10 ⊢ ((𝐺 ↾ 2o):2o⟶ℕ0 → (𝐺 ↾ 2o) Fn 2o)
121	119, 120	ax-mp 5	. . . . . . . . 9 ⊢ (𝐺 ↾ 2o) Fn 2o
122		fvres 5445	. . . . . . . . . . 11 ⊢ (𝑗 ∈ 2o → ((𝐺 ↾ 2o)‘𝑗) = (𝐺‘𝑗))
123		elpri 3550	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ {∅, 1o} → (𝑗 = ∅ ∨ 𝑗 = 1o))
124		df2o3 6327	. . . . . . . . . . . . 13 ⊢ 2o = {∅, 1o}
125	123, 124	eleq2s 2234	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ 2o → (𝑗 = ∅ ∨ 𝑗 = 1o))
126		fveq2 5421	. . . . . . . . . . . . . 14 ⊢ (𝑗 = ∅ → (𝐺‘𝑗) = (𝐺‘∅))
127		c0ex 7760	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ V
128	127	prid1 3629	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ {0, 1}
129	27, 128	eqeltri 2212	. . . . . . . . . . . . . 14 ⊢ (𝐺‘∅) ∈ {0, 1}
130	126, 129	eqeltrdi 2230	. . . . . . . . . . . . 13 ⊢ (𝑗 = ∅ → (𝐺‘𝑗) ∈ {0, 1})
131		fveq2 5421	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 1o → (𝐺‘𝑗) = (𝐺‘1o))
132		1ex 7761	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ V
133	132	prid2 3630	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ {0, 1}
134	44, 133	eqeltri 2212	. . . . . . . . . . . . . 14 ⊢ (𝐺‘1o) ∈ {0, 1}
135	131, 134	eqeltrdi 2230	. . . . . . . . . . . . 13 ⊢ (𝑗 = 1o → (𝐺‘𝑗) ∈ {0, 1})
136	130, 135	jaoi 705	. . . . . . . . . . . 12 ⊢ ((𝑗 = ∅ ∨ 𝑗 = 1o) → (𝐺‘𝑗) ∈ {0, 1})
137	125, 136	syl 14	. . . . . . . . . . 11 ⊢ (𝑗 ∈ 2o → (𝐺‘𝑗) ∈ {0, 1})
138	122, 137	eqeltrd 2216	. . . . . . . . . 10 ⊢ (𝑗 ∈ 2o → ((𝐺 ↾ 2o)‘𝑗) ∈ {0, 1})
139	138	rgen 2485	. . . . . . . . 9 ⊢ ∀𝑗 ∈ 2o ((𝐺 ↾ 2o)‘𝑗) ∈ {0, 1}
140		ffnfv 5578	. . . . . . . . 9 ⊢ ((𝐺 ↾ 2o):2o⟶{0, 1} ↔ ((𝐺 ↾ 2o) Fn 2o ∧ ∀𝑗 ∈ 2o ((𝐺 ↾ 2o)‘𝑗) ∈ {0, 1}))
141	121, 139, 140	mpbir2an 926	. . . . . . . 8 ⊢ (𝐺 ↾ 2o):2o⟶{0, 1}
142		elmapi 6564	. . . . . . . . 9 ⊢ (𝑔 ∈ (2o ↑𝑚 𝐴) → 𝑔:𝐴⟶2o)
143	142	adantl 275	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → 𝑔:𝐴⟶2o)
144		fco2 5289	. . . . . . . 8 ⊢ (((𝐺 ↾ 2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
145	141, 143, 144	sylancr 410	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
146		prexg 4133	. . . . . . . . . 10 ⊢ ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ∈ V)
147	14, 15, 146	mp2an 422	. . . . . . . . 9 ⊢ {0, 1} ∈ V
148	147	a1i 9	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → {0, 1} ∈ V)
149		simpll 518	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → 𝐴 ∈ 𝑉)
150	148, 149	elmapd 6556	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → ((𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚 𝐴) ↔ (𝐺 ∘ 𝑔):𝐴⟶{0, 1}))
151	145, 150	mpbird 166	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚 𝐴))
152	111, 112, 151	rspcdva 2794	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
153		nfcv 2281	. . . . . . . . . 10 ⊢ Ⅎ𝑥({0, 1} ↑𝑚 𝐴)
154		nfre1 2476	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0
155		nfra1 2466	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
156	154, 155	nfor 1553	. . . . . . . . . 10 ⊢ Ⅎ𝑥(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
157	153, 156	nfralxy 2471	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)
158	68, 157	nfan 1544	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
159		nfv 1508	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑔 ∈ (2o ↑𝑚 𝐴)
160	158, 159	nfan 1544	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴))
161	143	adantr 274	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶2o)
162	117	a1i 9	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 2o ⊆ ω)
163	161, 162	fssd 5285	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶ω)
164		simpr 109	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
165	163, 164	ffvelrnd 5556	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ω)
166		f1ocnvfv1 5678	. . . . . . . . . . 11 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑔‘𝑥) ∈ ω) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
167	10, 165, 166	sylancr 410	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
168	167	adantr 274	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
169		fvco3 5492	. . . . . . . . . . . . . 14 ⊢ ((𝑔:𝐴⟶2o ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
170	161, 169	sylancom 416	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
171	170	eqeq1d 2148	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 0 ↔ (𝐺‘(𝑔‘𝑥)) = 0))
172	171	biimpa 294	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (𝐺‘(𝑔‘𝑥)) = 0)
173	172	fveq2d 5425	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘0))
174	173, 31	syl6eq 2188	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = ∅)
175	168, 174	eqtr3d 2174	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (𝑔‘𝑥) = ∅)
176	175	exp31 361	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝑥 ∈ 𝐴 → (((𝐺 ∘ 𝑔)‘𝑥) = 0 → (𝑔‘𝑥) = ∅)))
177	160, 176	reximdai 2530	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0 → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
178	167	adantr 274	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
179	170	eqeq1d 2148	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔‘𝑥)) = 1))
180	179	biimpa 294	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (𝐺‘(𝑔‘𝑥)) = 1)
181	180	fveq2d 5425	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1))
182	181, 48	syl6eq 2188	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o)
183	178, 182	eqtr3d 2174	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (𝑔‘𝑥) = 1o)
184	183	ex 114	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 → (𝑔‘𝑥) = 1o))
185	160, 184	ralimdaa 2498	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
186	177, 185	orim12d 775	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → ((∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)))
187	152, 186	mpd 13	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
188	187	ralrimiva 2505	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
189	105, 188	impbida 585	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑔 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)))
190	1, 189	bitrd 187	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697   = wceq 1331  ⊤wtru 1332   ∈ wcel 1480  ∀wral 2416  ∃wrex 2417  Vcvv 2686   ⊆ wss 3071  ∅c0 3363  {cpr 3528   ↦ cmpt 3989  suc csuc 4287  ωcom 4504  ^◡ccnv 4538   ↾ cres 4541   ∘ ccom 4543   Fn wfn 5118  ⟶wf 5119  –1-1-onto→wf1o 5122  ‘cfv 5123  (class class class)co 5774  freccfrec 6287  1_oc1o 6306  2_oc2o 6307   ↑_𝑚 cmap 6542  Omnicomni 7004  0cc0 7620  1c1 7621   + caddc 7623  ℕ₀cn0 8977  ℤcz 9054

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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7711  ax-resscn 7712  ax-1cn 7713  ax-1re 7714  ax-icn 7715  ax-addcl 7716  ax-addrcl 7717  ax-mulcl 7718  ax-addcom 7720  ax-addass 7722  ax-distr 7724  ax-i2m1 7725  ax-0lt1 7726  ax-0id 7728  ax-rnegex 7729  ax-cnre 7731  ax-pre-ltirr 7732  ax-pre-ltwlin 7733  ax-pre-lttrn 7734  ax-pre-ltadd 7736

This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-recs 6202  df-frec 6288  df-1o 6313  df-2o 6314  df-map 6544  df-omni 7006  df-pnf 7802  df-mnf 7803  df-xr 7804  df-ltxr 7805  df-le 7806  df-sub 7935  df-neg 7936  df-inn 8721  df-n0 8978  df-z 9055  df-uz 9327

This theorem is referenced by:  isomninn  13226