Theorem ismkvnnlem 16837

Description: Lemma for ismkvnn 16838. 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 7445	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)))
2		nfv 1577	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑉
3		nfcv 2384	. . . . . . . . . 10 ⊢ Ⅎ𝑥(2o ↑𝑚 𝐴)
4		nfra1 2573	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
5	4	nfn 1706	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 ¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
6		nfre1 2585	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅
7	5, 6	nfim 1621	. . . . . . . . . 10 ⊢ Ⅎ𝑥(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)
8	3, 7	nfralxy 2580	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)
9	2, 8	nfan 1614	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
10		nfv 1577	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)
11	9, 10	nfan 1614	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴))
12		ismkvnnlem.g	. . . . . . . . . . . 12 ⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
13	12	frechashgf1o 10790	. . . . . . . . . . 11 ⊢ 𝐺:ω–1-1-onto→ℕ0
14		0nn0 9511	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
15		1nn0 9512	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ0
16		prssi 3852	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
17	14, 15, 16	mp2an 426	. . . . . . . . . . . 12 ⊢ {0, 1} ⊆ ℕ0
18		elmapi 6904	. . . . . . . . . . . . . 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 5813	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1})
22	17, 21	sselid 3236	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℕ0)
23		f1ocnvfv2 5951	. . . . . . . . . . 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 5748	. . . . . . . . . . . . . 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 2267	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (◡𝐺‘(𝑓‘𝑥)) = 1o)
31	30	fveq2d 5674	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o))
32		df-1o 6647	. . . . . . . . . . . 12 ⊢ 1o = suc ∅
33	32	fveq2i 5673	. . . . . . . . . . 11 ⊢ (𝐺‘1o) = (𝐺‘suc ∅)
34		0zd 9589	. . . . . . . . . . . . 13 ⊢ (⊤ → 0 ∈ ℤ)
35		peano1 4716	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ ω
36	35	a1i 9	. . . . . . . . . . . . 13 ⊢ (⊤ → ∅ ∈ ω)
37	34, 12, 36	frec2uzsucd 10763	. . . . . . . . . . . 12 ⊢ (⊤ → (𝐺‘suc ∅) = ((𝐺‘∅) + 1))
38	37	mptru 1407	. . . . . . . . . . 11 ⊢ (𝐺‘suc ∅) = ((𝐺‘∅) + 1)
39	34, 12	frec2uz0d 10761	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝐺‘∅) = 0)
40	39	mptru 1407	. . . . . . . . . . . . 13 ⊢ (𝐺‘∅) = 0
41	40	oveq1i 6060	. . . . . . . . . . . 12 ⊢ ((𝐺‘∅) + 1) = (0 + 1)
42		0p1e1 9351	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
43	41, 42	eqtri 2253	. . . . . . . . . . 11 ⊢ ((𝐺‘∅) + 1) = 1
44	33, 38, 43	3eqtri 2257	. . . . . . . . . 10 ⊢ (𝐺‘1o) = 1
45	31, 44	eqtrdi 2281	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1)
46	25, 45	eqtr3d 2267	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝑓‘𝑥) = 1)
47	46	ex 115	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → (𝑓‘𝑥) = 1))
48	11, 47	ralimdaa 2608	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
49	48	con3d 636	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
50		fveq1 5669	. . . . . . . . . 10 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (𝑔‘𝑥) = ((◡𝐺 ∘ 𝑓)‘𝑥))
51	50	eqeq1d 2241	. . . . . . . . 9 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = 1o ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
52	51	ralbidv 2542	. . . . . . . 8 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
53	52	notbid 673	. . . . . . 7 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
54	50	eqeq1d 2241	. . . . . . . 8 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = ∅ ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅))
55	54	rexbidv 2543	. . . . . . 7 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅))
56	53, 55	imbi12d 234	. . . . . 6 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅) ↔ (¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅)))
57		simplr 529	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
58	12	012of 16767	. . . . . . . 8 ⊢ (◡𝐺 ↾ {0, 1}):{0, 1}⟶2o
59	18	adantl 277	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝑓:𝐴⟶{0, 1})
60		fco2 5529	. . . . . . . 8 ⊢ (((◡𝐺 ↾ {0, 1}):{0, 1}⟶2o ∧ 𝑓:𝐴⟶{0, 1}) → (◡𝐺 ∘ 𝑓):𝐴⟶2o)
61	58, 59, 60	sylancr 414	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (◡𝐺 ∘ 𝑓):𝐴⟶2o)
62		2onn 6754	. . . . . . . . 9 ⊢ 2o ∈ ω
63	62	a1i 9	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 2o ∈ ω)
64		simpll 527	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝐴 ∈ 𝑉)
65	63, 64	elmapd 6896	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ((◡𝐺 ∘ 𝑓) ∈ (2o ↑𝑚 𝐴) ↔ (◡𝐺 ∘ 𝑓):𝐴⟶2o))
66	61, 65	mpbird 167	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (◡𝐺 ∘ 𝑓) ∈ (2o ↑𝑚 𝐴))
67	56, 57, 66	rspcdva 2926	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅))
68	24	adantr 276	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
69	27	eqeq1d 2241	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ ↔ (◡𝐺‘(𝑓‘𝑥)) = ∅))
70	69	biimpa 296	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (◡𝐺‘(𝑓‘𝑥)) = ∅)
71	70	fveq2d 5674	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘∅))
72	71, 40	eqtrdi 2281	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 0)
73	68, 72	eqtr3d 2267	. . . . . . 7 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝑓‘𝑥) = 0)
74	73	exp31 364	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝑥 ∈ 𝐴 → (((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ → (𝑓‘𝑥) = 0)))
75	11, 74	reximdai 2640	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
76	49, 67, 75	3syld 57	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
77	76	ralrimiva 2615	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
78		nfcv 2384	. . . . . . . . . 10 ⊢ Ⅎ𝑥({0, 1} ↑𝑚 𝐴)
79		nfra1 2573	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
80	79	nfn 1706	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 ¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
81		nfre1 2585	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0
82	80, 81	nfim 1621	. . . . . . . . . 10 ⊢ Ⅎ𝑥(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)
83	78, 82	nfralxy 2580	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)
84	2, 83	nfan 1614	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
85		nfv 1577	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑔 ∈ (2o ↑𝑚 𝐴)
86	84, 85	nfan 1614	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴))
87		elmapi 6904	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ (2o ↑𝑚 𝐴) → 𝑔:𝐴⟶2o)
88	87	ad2antlr 489	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶2o)
89		omelon 4731	. . . . . . . . . . . . . . . 16 ⊢ ω ∈ On
90	89	onelssi 4550	. . . . . . . . . . . . . . 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 5522	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶ω)
94		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
95	93, 94	ffvelcdmd 5813	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ω)
96		f1ocnvfv1 5950	. . . . . . . . . . 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 5748	. . . . . . . . . . . . . 14 ⊢ ((𝑔:𝐴⟶2o ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
100	88, 99	sylancom 420	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
101	100	eqeq1d 2241	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔‘𝑥)) = 1))
102	101	biimpa 296	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (𝐺‘(𝑔‘𝑥)) = 1)
103	102	fveq2d 5674	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1))
104		1onn 6753	. . . . . . . . . . . 12 ⊢ 1o ∈ ω
105		f1ocnvfv 5952	. . . . . . . . . . . 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 2281	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o)
109	98, 108	eqtr3d 2267	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (𝑔‘𝑥) = 1o)
110	109	ex 115	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 → (𝑔‘𝑥) = 1o))
111	86, 110	ralimdaa 2608	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
112	111	con3d 636	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
113		fveq1 5669	. . . . . . . . . 10 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (𝑓‘𝑥) = ((𝐺 ∘ 𝑔)‘𝑥))
114	113	eqeq1d 2241	. . . . . . . . 9 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 1 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 1))
115	114	ralbidv 2542	. . . . . . . 8 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
116	115	notbid 673	. . . . . . 7 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
117	113	eqeq1d 2241	. . . . . . . 8 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 0 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 0))
118	117	rexbidv 2543	. . . . . . 7 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ↔ ∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0))
119	116, 118	imbi12d 234	. . . . . 6 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0) ↔ (¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0)))
120		simplr 529	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
121	12	2o01f 16768	. . . . . . . 8 ⊢ (𝐺 ↾ 2o):2o⟶{0, 1}
122	87	adantl 277	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → 𝑔:𝐴⟶2o)
123		fco2 5529	. . . . . . . 8 ⊢ (((𝐺 ↾ 2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
124	121, 122, 123	sylancr 414	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
125		prexg 4325	. . . . . . . . . 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 6896	. . . . . . 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 2926	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0))
132	97	adantr 276	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
133	100	eqeq1d 2241	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 0 ↔ (𝐺‘(𝑔‘𝑥)) = 0))
134	133	biimpa 296	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (𝐺‘(𝑔‘𝑥)) = 0)
135	134	fveq2d 5674	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘0))
136		f1ocnvfv 5952	. . . . . . . . . . 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 2281	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = ∅)
140	132, 139	eqtr3d 2267	. . . . . . 7 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (𝑔‘𝑥) = ∅)
141	140	exp31 364	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝑥 ∈ 𝐴 → (((𝐺 ∘ 𝑔)‘𝑥) = 0 → (𝑔‘𝑥) = ∅)))
142	86, 141	reximdai 2640	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0 → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
143	112, 131, 142	3syld 57	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
144	143	ralrimiva 2615	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
145	77, 144	impbida 600	. 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 1398  ⊤wtru 1399   ∈ wcel 2203  ∀wral 2520  ∃wrex 2521  Vcvv 2813   ⊆ wss 3211  ∅c0 3508  {cpr 3690   ↦ cmpt 4171  suc csuc 4486  ωcom 4712  ^◡ccnv 4748   ↾ cres 4751   ∘ ccom 4753  ⟶wf 5348  –1-1-onto→wf1o 5351  ‘cfv 5352  (class class class)co 6050  freccfrec 6621  1_oc1o 6640  2_oc2o 6641   ↑_𝑚 cmap 6882  Markovcmarkov 7442  0cc0 8127  1c1 8128   + caddc 8130  ℕ₀cn0 9496  ℤcz 9577

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-coll 4225  ax-sep 4228  ax-nul 4236  ax-pow 4287  ax-pr 4322  ax-un 4554  ax-setind 4659  ax-iinf 4710  ax-cnex 8218  ax-resscn 8219  ax-1cn 8220  ax-1re 8221  ax-icn 8222  ax-addcl 8223  ax-addrcl 8224  ax-mulcl 8225  ax-addcom 8227  ax-addass 8229  ax-distr 8231  ax-i2m1 8232  ax-0lt1 8233  ax-0id 8235  ax-rnegex 8236  ax-cnre 8238  ax-pre-ltirr 8239  ax-pre-ltwlin 8240  ax-pre-lttrn 8241  ax-pre-ltadd 8243

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2815  df-sbc 3043  df-csb 3139  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-nul 3509  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-int 3950  df-iun 3993  df-br 4110  df-opab 4172  df-mpt 4173  df-tr 4209  df-id 4414  df-iord 4487  df-on 4489  df-ilim 4490  df-suc 4492  df-iom 4713  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-res 4761  df-ima 4762  df-iota 5312  df-fun 5354  df-fn 5355  df-f 5356  df-f1 5357  df-fo 5358  df-f1o 5359  df-fv 5360  df-riota 6003  df-ov 6053  df-oprab 6054  df-mpo 6055  df-recs 6536  df-frec 6622  df-1o 6647  df-2o 6648  df-map 6884  df-markov 7443  df-pnf 8310  df-mnf 8311  df-xr 8312  df-ltxr 8313  df-le 8314  df-sub 8446  df-neg 8447  df-inn 9238  df-n0 9497  df-z 9578  df-uz 9854

This theorem is referenced by:  ismkvnn  16838