Theorem ismkvnnlem 16480

Description: Lemma for ismkvnn 16481. The result, with a hypothesis to give a name to an expression for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)

Hypothesis

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

Assertion

Ref	Expression
ismkvnnlem	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)))

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

Proof of Theorem ismkvnnlem

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ismkvmap 7332	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)))
2		nfv 1574	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑉
3		nfcv 2372	. . . . . . . . . 10 ⊢ Ⅎ𝑥(2o ↑𝑚 𝐴)
4		nfra1 2561	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
5	4	nfn 1704	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 ¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
6		nfre1 2573	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅
7	5, 6	nfim 1618	. . . . . . . . . 10 ⊢ Ⅎ𝑥(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)
8	3, 7	nfralxy 2568	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)
9	2, 8	nfan 1611	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
10		nfv 1574	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)
11	9, 10	nfan 1611	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴))
12		ismkvnnlem.g	. . . . . . . . . . . 12 ⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
13	12	frechashgf1o 10662	. . . . . . . . . . 11 ⊢ 𝐺:ω–1-1-onto→ℕ0
14		0nn0 9395	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
15		1nn0 9396	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ0
16		prssi 3826	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
17	14, 15, 16	mp2an 426	. . . . . . . . . . . 12 ⊢ {0, 1} ⊆ ℕ0
18		elmapi 6825	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ({0, 1} ↑𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
19	18	ad2antlr 489	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1})
20		simpr 110	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
21	19, 20	ffvelcdmd 5773	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1})
22	17, 21	sselid 3222	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℕ0)
23		f1ocnvfv2 5908	. . . . . . . . . . 11 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑓‘𝑥) ∈ ℕ0) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
24	13, 22, 23	sylancr 414	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
25	24	adantr 276	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
26		fvco3 5707	. . . . . . . . . . . . . 14 ⊢ ((𝑓:𝐴⟶{0, 1} ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
27	19, 26	sylancom 420	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
28	27	adantr 276	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
29		simpr 110	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)
30	28, 29	eqtr3d 2264	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (◡𝐺‘(𝑓‘𝑥)) = 1o)
31	30	fveq2d 5633	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o))
32		df-1o 6568	. . . . . . . . . . . 12 ⊢ 1o = suc ∅
33	32	fveq2i 5632	. . . . . . . . . . 11 ⊢ (𝐺‘1o) = (𝐺‘suc ∅)
34		0zd 9469	. . . . . . . . . . . . 13 ⊢ (⊤ → 0 ∈ ℤ)
35		peano1 4686	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ ω
36	35	a1i 9	. . . . . . . . . . . . 13 ⊢ (⊤ → ∅ ∈ ω)
37	34, 12, 36	frec2uzsucd 10635	. . . . . . . . . . . 12 ⊢ (⊤ → (𝐺‘suc ∅) = ((𝐺‘∅) + 1))
38	37	mptru 1404	. . . . . . . . . . 11 ⊢ (𝐺‘suc ∅) = ((𝐺‘∅) + 1)
39	34, 12	frec2uz0d 10633	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝐺‘∅) = 0)
40	39	mptru 1404	. . . . . . . . . . . . 13 ⊢ (𝐺‘∅) = 0
41	40	oveq1i 6017	. . . . . . . . . . . 12 ⊢ ((𝐺‘∅) + 1) = (0 + 1)
42		0p1e1 9235	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
43	41, 42	eqtri 2250	. . . . . . . . . . 11 ⊢ ((𝐺‘∅) + 1) = 1
44	33, 38, 43	3eqtri 2254	. . . . . . . . . 10 ⊢ (𝐺‘1o) = 1
45	31, 44	eqtrdi 2278	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1)
46	25, 45	eqtr3d 2264	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝑓‘𝑥) = 1)
47	46	ex 115	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → (𝑓‘𝑥) = 1))
48	11, 47	ralimdaa 2596	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
49	48	con3d 634	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
50		fveq1 5628	. . . . . . . . . 10 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (𝑔‘𝑥) = ((◡𝐺 ∘ 𝑓)‘𝑥))
51	50	eqeq1d 2238	. . . . . . . . 9 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = 1o ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
52	51	ralbidv 2530	. . . . . . . 8 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
53	52	notbid 671	. . . . . . 7 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
54	50	eqeq1d 2238	. . . . . . . 8 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = ∅ ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅))
55	54	rexbidv 2531	. . . . . . 7 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅))
56	53, 55	imbi12d 234	. . . . . 6 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅) ↔ (¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅)))
57		simplr 528	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
58	12	012of 16416	. . . . . . . 8 ⊢ (◡𝐺 ↾ {0, 1}):{0, 1}⟶2o
59	18	adantl 277	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝑓:𝐴⟶{0, 1})
60		fco2 5492	. . . . . . . 8 ⊢ (((◡𝐺 ↾ {0, 1}):{0, 1}⟶2o ∧ 𝑓:𝐴⟶{0, 1}) → (◡𝐺 ∘ 𝑓):𝐴⟶2o)
61	58, 59, 60	sylancr 414	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (◡𝐺 ∘ 𝑓):𝐴⟶2o)
62		2onn 6675	. . . . . . . . 9 ⊢ 2o ∈ ω
63	62	a1i 9	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 2o ∈ ω)
64		simpll 527	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝐴 ∈ 𝑉)
65	63, 64	elmapd 6817	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ((◡𝐺 ∘ 𝑓) ∈ (2o ↑𝑚 𝐴) ↔ (◡𝐺 ∘ 𝑓):𝐴⟶2o))
66	61, 65	mpbird 167	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (◡𝐺 ∘ 𝑓) ∈ (2o ↑𝑚 𝐴))
67	56, 57, 66	rspcdva 2912	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅))
68	24	adantr 276	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
69	27	eqeq1d 2238	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ ↔ (◡𝐺‘(𝑓‘𝑥)) = ∅))
70	69	biimpa 296	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (◡𝐺‘(𝑓‘𝑥)) = ∅)
71	70	fveq2d 5633	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘∅))
72	71, 40	eqtrdi 2278	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 0)
73	68, 72	eqtr3d 2264	. . . . . . 7 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝑓‘𝑥) = 0)
74	73	exp31 364	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝑥 ∈ 𝐴 → (((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ → (𝑓‘𝑥) = 0)))
75	11, 74	reximdai 2628	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
76	49, 67, 75	3syld 57	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
77	76	ralrimiva 2603	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
78		nfcv 2372	. . . . . . . . . 10 ⊢ Ⅎ𝑥({0, 1} ↑𝑚 𝐴)
79		nfra1 2561	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
80	79	nfn 1704	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 ¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
81		nfre1 2573	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0
82	80, 81	nfim 1618	. . . . . . . . . 10 ⊢ Ⅎ𝑥(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)
83	78, 82	nfralxy 2568	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)
84	2, 83	nfan 1611	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
85		nfv 1574	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑔 ∈ (2o ↑𝑚 𝐴)
86	84, 85	nfan 1611	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴))
87		elmapi 6825	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ (2o ↑𝑚 𝐴) → 𝑔:𝐴⟶2o)
88	87	ad2antlr 489	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶2o)
89		omelon 4701	. . . . . . . . . . . . . . . 16 ⊢ ω ∈ On
90	89	onelssi 4520	. . . . . . . . . . . . . . 15 ⊢ (2o ∈ ω → 2o ⊆ ω)
91	62, 90	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 2o ⊆ ω
92	91	a1i 9	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 2o ⊆ ω)
93	88, 92	fssd 5486	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶ω)
94		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
95	93, 94	ffvelcdmd 5773	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ω)
96		f1ocnvfv1 5907	. . . . . . . . . . 11 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑔‘𝑥) ∈ ω) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
97	13, 95, 96	sylancr 414	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
98	97	adantr 276	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
99		fvco3 5707	. . . . . . . . . . . . . 14 ⊢ ((𝑔:𝐴⟶2o ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
100	88, 99	sylancom 420	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
101	100	eqeq1d 2238	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔‘𝑥)) = 1))
102	101	biimpa 296	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (𝐺‘(𝑔‘𝑥)) = 1)
103	102	fveq2d 5633	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1))
104		1onn 6674	. . . . . . . . . . . 12 ⊢ 1o ∈ ω
105		f1ocnvfv 5909	. . . . . . . . . . . 12 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ 1o ∈ ω) → ((𝐺‘1o) = 1 → (◡𝐺‘1) = 1o))
106	13, 104, 105	mp2an 426	. . . . . . . . . . 11 ⊢ ((𝐺‘1o) = 1 → (◡𝐺‘1) = 1o)
107	44, 106	ax-mp 5	. . . . . . . . . 10 ⊢ (◡𝐺‘1) = 1o
108	103, 107	eqtrdi 2278	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o)
109	98, 108	eqtr3d 2264	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (𝑔‘𝑥) = 1o)
110	109	ex 115	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 → (𝑔‘𝑥) = 1o))
111	86, 110	ralimdaa 2596	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
112	111	con3d 634	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
113		fveq1 5628	. . . . . . . . . 10 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (𝑓‘𝑥) = ((𝐺 ∘ 𝑔)‘𝑥))
114	113	eqeq1d 2238	. . . . . . . . 9 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 1 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 1))
115	114	ralbidv 2530	. . . . . . . 8 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
116	115	notbid 671	. . . . . . 7 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
117	113	eqeq1d 2238	. . . . . . . 8 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 0 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 0))
118	117	rexbidv 2531	. . . . . . 7 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ↔ ∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0))
119	116, 118	imbi12d 234	. . . . . 6 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0) ↔ (¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0)))
120		simplr 528	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
121	12	2o01f 16417	. . . . . . . 8 ⊢ (𝐺 ↾ 2o):2o⟶{0, 1}
122	87	adantl 277	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → 𝑔:𝐴⟶2o)
123		fco2 5492	. . . . . . . 8 ⊢ (((𝐺 ↾ 2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
124	121, 122, 123	sylancr 414	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
125		prexg 4295	. . . . . . . . . 10 ⊢ ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ∈ V)
126	14, 15, 125	mp2an 426	. . . . . . . . 9 ⊢ {0, 1} ∈ V
127	126	a1i 9	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → {0, 1} ∈ V)
128		simpll 527	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → 𝐴 ∈ 𝑉)
129	127, 128	elmapd 6817	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → ((𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚 𝐴) ↔ (𝐺 ∘ 𝑔):𝐴⟶{0, 1}))
130	124, 129	mpbird 167	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚 𝐴))
131	119, 120, 130	rspcdva 2912	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0))
132	97	adantr 276	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
133	100	eqeq1d 2238	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 0 ↔ (𝐺‘(𝑔‘𝑥)) = 0))
134	133	biimpa 296	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (𝐺‘(𝑔‘𝑥)) = 0)
135	134	fveq2d 5633	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘0))
136		f1ocnvfv 5909	. . . . . . . . . . 11 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ ∅ ∈ ω) → ((𝐺‘∅) = 0 → (◡𝐺‘0) = ∅))
137	13, 35, 136	mp2an 426	. . . . . . . . . 10 ⊢ ((𝐺‘∅) = 0 → (◡𝐺‘0) = ∅)
138	40, 137	ax-mp 5	. . . . . . . . 9 ⊢ (◡𝐺‘0) = ∅
139	135, 138	eqtrdi 2278	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = ∅)
140	132, 139	eqtr3d 2264	. . . . . . 7 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (𝑔‘𝑥) = ∅)
141	140	exp31 364	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝑥 ∈ 𝐴 → (((𝐺 ∘ 𝑔)‘𝑥) = 0 → (𝑔‘𝑥) = ∅)))
142	86, 141	reximdai 2628	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0 → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
143	112, 131, 142	3syld 57	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
144	143	ralrimiva 2603	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
145	77, 144	impbida 598	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅) ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)))
146	1, 145	bitrd 188	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395  ⊤wtru 1396   ∈ wcel 2200  ∀wral 2508  ∃wrex 2509  Vcvv 2799   ⊆ wss 3197  ∅c0 3491  {cpr 3667   ↦ cmpt 4145  suc csuc 4456  ωcom 4682  ^◡ccnv 4718   ↾ cres 4721   ∘ ccom 4723  ⟶wf 5314  –1-1-onto→wf1o 5317  ‘cfv 5318  (class class class)co 6007  freccfrec 6542  1_oc1o 6561  2_oc2o 6562   ↑_𝑚 cmap 6803  Markovcmarkov 7329  0cc0 8010  1c1 8011   + caddc 8013  ℕ₀cn0 9380  ℤcz 9457

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4199  ax-sep 4202  ax-nul 4210  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-iinf 4680  ax-cnex 8101  ax-resscn 8102  ax-1cn 8103  ax-1re 8104  ax-icn 8105  ax-addcl 8106  ax-addrcl 8107  ax-mulcl 8108  ax-addcom 8110  ax-addass 8112  ax-distr 8114  ax-i2m1 8115  ax-0lt1 8116  ax-0id 8118  ax-rnegex 8119  ax-cnre 8121  ax-pre-ltirr 8122  ax-pre-ltwlin 8123  ax-pre-lttrn 8124  ax-pre-ltadd 8126

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-nul 3492  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-iun 3967  df-br 4084  df-opab 4146  df-mpt 4147  df-tr 4183  df-id 4384  df-iord 4457  df-on 4459  df-ilim 4460  df-suc 4462  df-iom 4683  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-res 4731  df-ima 4732  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-f1 5323  df-fo 5324  df-f1o 5325  df-fv 5326  df-riota 5960  df-ov 6010  df-oprab 6011  df-mpo 6012  df-recs 6457  df-frec 6543  df-1o 6568  df-2o 6569  df-map 6805  df-markov 7330  df-pnf 8194  df-mnf 8195  df-xr 8196  df-ltxr 8197  df-le 8198  df-sub 8330  df-neg 8331  df-inn 9122  df-n0 9381  df-z 9458  df-uz 9734

This theorem is referenced by:  ismkvnn  16481