Theorem ismkvnnlem 14084

Description: Lemma for ismkvnn 14085. 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 7130	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)))
2		nfv 1521	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑉
3		nfcv 2312	. . . . . . . . . 10 ⊢ Ⅎ𝑥(2o ↑𝑚 𝐴)
4		nfra1 2501	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
5	4	nfn 1651	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 ¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o
6		nfre1 2513	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅
7	5, 6	nfim 1565	. . . . . . . . . 10 ⊢ Ⅎ𝑥(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)
8	3, 7	nfralxy 2508	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)
9	2, 8	nfan 1558	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
10		nfv 1521	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)
11	9, 10	nfan 1558	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴))
12		ismkvnnlem.g	. . . . . . . . . . . 12 ⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
13	12	frechashgf1o 10384	. . . . . . . . . . 11 ⊢ 𝐺:ω–1-1-onto→ℕ0
14		0nn0 9150	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
15		1nn0 9151	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ0
16		prssi 3738	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
17	14, 15, 16	mp2an 424	. . . . . . . . . . . 12 ⊢ {0, 1} ⊆ ℕ0
18		elmapi 6648	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ({0, 1} ↑𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
19	18	ad2antlr 486	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1})
20		simpr 109	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
21	19, 20	ffvelrnd 5632	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1})
22	17, 21	sselid 3145	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℕ0)
23		f1ocnvfv2 5757	. . . . . . . . . . 11 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑓‘𝑥) ∈ ℕ0) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
24	13, 22, 23	sylancr 412	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
25	24	adantr 274	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
26		fvco3 5567	. . . . . . . . . . . . . 14 ⊢ ((𝑓:𝐴⟶{0, 1} ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
27	19, 26	sylancom 418	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
28	27	adantr 274	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥)))
29		simpr 109	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)
30	28, 29	eqtr3d 2205	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (◡𝐺‘(𝑓‘𝑥)) = 1o)
31	30	fveq2d 5500	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o))
32		df-1o 6395	. . . . . . . . . . . 12 ⊢ 1o = suc ∅
33	32	fveq2i 5499	. . . . . . . . . . 11 ⊢ (𝐺‘1o) = (𝐺‘suc ∅)
34		0zd 9224	. . . . . . . . . . . . 13 ⊢ (⊤ → 0 ∈ ℤ)
35		peano1 4578	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ ω
36	35	a1i 9	. . . . . . . . . . . . 13 ⊢ (⊤ → ∅ ∈ ω)
37	34, 12, 36	frec2uzsucd 10357	. . . . . . . . . . . 12 ⊢ (⊤ → (𝐺‘suc ∅) = ((𝐺‘∅) + 1))
38	37	mptru 1357	. . . . . . . . . . 11 ⊢ (𝐺‘suc ∅) = ((𝐺‘∅) + 1)
39	34, 12	frec2uz0d 10355	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝐺‘∅) = 0)
40	39	mptru 1357	. . . . . . . . . . . . 13 ⊢ (𝐺‘∅) = 0
41	40	oveq1i 5863	. . . . . . . . . . . 12 ⊢ ((𝐺‘∅) + 1) = (0 + 1)
42		0p1e1 8992	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
43	41, 42	eqtri 2191	. . . . . . . . . . 11 ⊢ ((𝐺‘∅) + 1) = 1
44	33, 38, 43	3eqtri 2195	. . . . . . . . . 10 ⊢ (𝐺‘1o) = 1
45	31, 44	eqtrdi 2219	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1)
46	25, 45	eqtr3d 2205	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝑓‘𝑥) = 1)
47	46	ex 114	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → (𝑓‘𝑥) = 1))
48	11, 47	ralimdaa 2536	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
49	48	con3d 626	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
50		fveq1 5495	. . . . . . . . . 10 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (𝑔‘𝑥) = ((◡𝐺 ∘ 𝑓)‘𝑥))
51	50	eqeq1d 2179	. . . . . . . . 9 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = 1o ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
52	51	ralbidv 2470	. . . . . . . 8 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
53	52	notbid 662	. . . . . . 7 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))
54	50	eqeq1d 2179	. . . . . . . 8 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = ∅ ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅))
55	54	rexbidv 2471	. . . . . . 7 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅))
56	53, 55	imbi12d 233	. . . . . 6 ⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅) ↔ (¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅)))
57		simplr 525	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
58	12	012of 14028	. . . . . . . 8 ⊢ (◡𝐺 ↾ {0, 1}):{0, 1}⟶2o
59	18	adantl 275	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝑓:𝐴⟶{0, 1})
60		fco2 5364	. . . . . . . 8 ⊢ (((◡𝐺 ↾ {0, 1}):{0, 1}⟶2o ∧ 𝑓:𝐴⟶{0, 1}) → (◡𝐺 ∘ 𝑓):𝐴⟶2o)
61	58, 59, 60	sylancr 412	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (◡𝐺 ∘ 𝑓):𝐴⟶2o)
62		2onn 6500	. . . . . . . . 9 ⊢ 2o ∈ ω
63	62	a1i 9	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 2o ∈ ω)
64		simpll 524	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → 𝐴 ∈ 𝑉)
65	63, 64	elmapd 6640	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → ((◡𝐺 ∘ 𝑓) ∈ (2o ↑𝑚 𝐴) ↔ (◡𝐺 ∘ 𝑓):𝐴⟶2o))
66	61, 65	mpbird 166	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (◡𝐺 ∘ 𝑓) ∈ (2o ↑𝑚 𝐴))
67	56, 57, 66	rspcdva 2839	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅))
68	24	adantr 274	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥))
69	27	eqeq1d 2179	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ ↔ (◡𝐺‘(𝑓‘𝑥)) = ∅))
70	69	biimpa 294	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (◡𝐺‘(𝑓‘𝑥)) = ∅)
71	70	fveq2d 5500	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘∅))
72	71, 40	eqtrdi 2219	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 0)
73	68, 72	eqtr3d 2205	. . . . . . 7 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝑓‘𝑥) = 0)
74	73	exp31 362	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (𝑥 ∈ 𝐴 → (((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ → (𝑓‘𝑥) = 0)))
75	11, 74	reximdai 2568	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
76	49, 67, 75	3syld 57	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
77	76	ralrimiva 2543	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
78		nfcv 2312	. . . . . . . . . 10 ⊢ Ⅎ𝑥({0, 1} ↑𝑚 𝐴)
79		nfra1 2501	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
80	79	nfn 1651	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 ¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1
81		nfre1 2513	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0
82	80, 81	nfim 1565	. . . . . . . . . 10 ⊢ Ⅎ𝑥(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)
83	78, 82	nfralxy 2508	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)
84	2, 83	nfan 1558	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
85		nfv 1521	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑔 ∈ (2o ↑𝑚 𝐴)
86	84, 85	nfan 1558	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴))
87		elmapi 6648	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ (2o ↑𝑚 𝐴) → 𝑔:𝐴⟶2o)
88	87	ad2antlr 486	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶2o)
89		omelon 4593	. . . . . . . . . . . . . . . 16 ⊢ ω ∈ On
90	89	onelssi 4414	. . . . . . . . . . . . . . 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 5360	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶ω)
94		simpr 109	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
95	93, 94	ffvelrnd 5632	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ω)
96		f1ocnvfv1 5756	. . . . . . . . . . 11 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑔‘𝑥) ∈ ω) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
97	13, 95, 96	sylancr 412	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
98	97	adantr 274	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
99		fvco3 5567	. . . . . . . . . . . . . 14 ⊢ ((𝑔:𝐴⟶2o ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
100	88, 99	sylancom 418	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥)))
101	100	eqeq1d 2179	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔‘𝑥)) = 1))
102	101	biimpa 294	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (𝐺‘(𝑔‘𝑥)) = 1)
103	102	fveq2d 5500	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1))
104		1onn 6499	. . . . . . . . . . . 12 ⊢ 1o ∈ ω
105		f1ocnvfv 5758	. . . . . . . . . . . 12 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ 1o ∈ ω) → ((𝐺‘1o) = 1 → (◡𝐺‘1) = 1o))
106	13, 104, 105	mp2an 424	. . . . . . . . . . 11 ⊢ ((𝐺‘1o) = 1 → (◡𝐺‘1) = 1o)
107	44, 106	ax-mp 5	. . . . . . . . . 10 ⊢ (◡𝐺‘1) = 1o
108	103, 107	eqtrdi 2219	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o)
109	98, 108	eqtr3d 2205	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (𝑔‘𝑥) = 1o)
110	109	ex 114	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 → (𝑔‘𝑥) = 1o))
111	86, 110	ralimdaa 2536	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))
112	111	con3d 626	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
113		fveq1 5495	. . . . . . . . . 10 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (𝑓‘𝑥) = ((𝐺 ∘ 𝑔)‘𝑥))
114	113	eqeq1d 2179	. . . . . . . . 9 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 1 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 1))
115	114	ralbidv 2470	. . . . . . . 8 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
116	115	notbid 662	. . . . . . 7 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))
117	113	eqeq1d 2179	. . . . . . . 8 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 0 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 0))
118	117	rexbidv 2471	. . . . . . 7 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ↔ ∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0))
119	116, 118	imbi12d 233	. . . . . 6 ⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0) ↔ (¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0)))
120		simplr 525	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
121	12	2o01f 14029	. . . . . . . 8 ⊢ (𝐺 ↾ 2o):2o⟶{0, 1}
122	87	adantl 275	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → 𝑔:𝐴⟶2o)
123		fco2 5364	. . . . . . . 8 ⊢ (((𝐺 ↾ 2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
124	121, 122, 123	sylancr 412	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1})
125		prexg 4196	. . . . . . . . . 10 ⊢ ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ∈ V)
126	14, 15, 125	mp2an 424	. . . . . . . . 9 ⊢ {0, 1} ∈ V
127	126	a1i 9	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → {0, 1} ∈ V)
128		simpll 524	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → 𝐴 ∈ 𝑉)
129	127, 128	elmapd 6640	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → ((𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚 𝐴) ↔ (𝐺 ∘ 𝑔):𝐴⟶{0, 1}))
130	124, 129	mpbird 166	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚 𝐴))
131	119, 120, 130	rspcdva 2839	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0))
132	97	adantr 274	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥))
133	100	eqeq1d 2179	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 0 ↔ (𝐺‘(𝑔‘𝑥)) = 0))
134	133	biimpa 294	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (𝐺‘(𝑔‘𝑥)) = 0)
135	134	fveq2d 5500	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘0))
136		f1ocnvfv 5758	. . . . . . . . . . 11 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ ∅ ∈ ω) → ((𝐺‘∅) = 0 → (◡𝐺‘0) = ∅))
137	13, 35, 136	mp2an 424	. . . . . . . . . 10 ⊢ ((𝐺‘∅) = 0 → (◡𝐺‘0) = ∅)
138	40, 137	ax-mp 5	. . . . . . . . 9 ⊢ (◡𝐺‘0) = ∅
139	135, 138	eqtrdi 2219	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = ∅)
140	132, 139	eqtr3d 2205	. . . . . . 7 ⊢ (((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (𝑔‘𝑥) = ∅)
141	140	exp31 362	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (𝑥 ∈ 𝐴 → (((𝐺 ∘ 𝑔)‘𝑥) = 0 → (𝑔‘𝑥) = ∅)))
142	86, 141	reximdai 2568	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0 → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
143	112, 131, 142	3syld 57	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o ↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
144	143	ralrimiva 2543	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) → ∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))
145	77, 144	impbida 591	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑔 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅) ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)))
146	1, 145	bitrd 187	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1348  ⊤wtru 1349   ∈ wcel 2141  ∀wral 2448  ∃wrex 2449  Vcvv 2730   ⊆ wss 3121  ∅c0 3414  {cpr 3584   ↦ cmpt 4050  suc csuc 4350  ωcom 4574  ^◡ccnv 4610   ↾ cres 4613   ∘ ccom 4615  ⟶wf 5194  –1-1-onto→wf1o 5197  ‘cfv 5198  (class class class)co 5853  freccfrec 6369  1_oc1o 6388  2_oc2o 6389   ↑_𝑚 cmap 6626  Markovcmarkov 7127  0cc0 7774  1c1 7775   + caddc 7777  ℕ₀cn0 9135  ℤcz 9212

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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572  ax-cnex 7865  ax-resscn 7866  ax-1cn 7867  ax-1re 7868  ax-icn 7869  ax-addcl 7870  ax-addrcl 7871  ax-mulcl 7872  ax-addcom 7874  ax-addass 7876  ax-distr 7878  ax-i2m1 7879  ax-0lt1 7880  ax-0id 7882  ax-rnegex 7883  ax-cnre 7885  ax-pre-ltirr 7886  ax-pre-ltwlin 7887  ax-pre-lttrn 7888  ax-pre-ltadd 7890

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-iord 4351  df-on 4353  df-ilim 4354  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-riota 5809  df-ov 5856  df-oprab 5857  df-mpo 5858  df-recs 6284  df-frec 6370  df-1o 6395  df-2o 6396  df-map 6628  df-markov 7128  df-pnf 7956  df-mnf 7957  df-xr 7958  df-ltxr 7959  df-le 7960  df-sub 8092  df-neg 8093  df-inn 8879  df-n0 9136  df-z 9213  df-uz 9488

This theorem is referenced by:  ismkvnn  14085