iswomni0 - Mathbox for Jim Kingdon

	Mathbox for Jim Kingdon		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > Mathboxes > iswomni0		GIF version

Theorem iswomni0 16828

Description: Weak omniscience stated in terms of equality with 0. Like iswomninn 16827 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.)

**Assertion**
Ref	Expression
iswomni0	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))

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

Proof of Theorem iswomni0 Dummy variables 𝑔 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iswomninn 16827	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
2		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (𝑓‘𝑧) = 0)
3	2	oveq2d 6065	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (1 − (𝑓‘𝑧)) = (1 − 0))
4		1m0e1 9349	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
5	3, 4	eqtrdi 2281	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (1 − (𝑓‘𝑧)) = 1)
6		1ex 8268	. . . . . . . . . . 11 ⊢ 1 ∈ V
7	6	prid2 3797	. . . . . . . . . 10 ⊢ 1 ∈ {0, 1}
8	5, 7	eqeltrdi 2323	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (1 − (𝑓‘𝑧)) ∈ {0, 1})
9		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (𝑓‘𝑧) = 1)
10	9	oveq2d 6065	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) = (1 − 1))
11		1m1e0 9305	. . . . . . . . . . 11 ⊢ (1 − 1) = 0
12	10, 11	eqtrdi 2281	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) = 0)
13		c0ex 8267	. . . . . . . . . . 11 ⊢ 0 ∈ V
14	13	prid1 3796	. . . . . . . . . 10 ⊢ 0 ∈ {0, 1}
15	12, 14	eqeltrdi 2323	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) ∈ {0, 1})
16		elmapi 6903	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ ({0, 1} ↑_𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
17	16	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1})
18		simpr 110	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
19	17, 18	ffvelcdmd 5812	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑓‘𝑧) ∈ {0, 1})
20		elpri 3711	. . . . . . . . . 10 ⊢ ((𝑓‘𝑧) ∈ {0, 1} → ((𝑓‘𝑧) = 0 ∨ (𝑓‘𝑧) = 1))
21	19, 20	syl 14	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → ((𝑓‘𝑧) = 0 ∨ (𝑓‘𝑧) = 1))
22	8, 15, 21	mpjaodan 806	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (1 − (𝑓‘𝑧)) ∈ {0, 1})
23	22	fmpttd 5831	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))):𝐴⟶{0, 1})
24		0nn0 9510	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
25		1nn0 9511	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
26		prexg 4324	. . . . . . . . . 10 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) → {0, 1} ∈ V)
27	24, 25, 26	mp2an 426	. . . . . . . . 9 ⊢ {0, 1} ∈ V
28	27	a1i 9	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → {0, 1} ∈ V)
29		simpl 109	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → 𝐴 ∈ 𝑉)
30	28, 29	elmapd 6895	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴) ↔ (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))):𝐴⟶{0, 1}))
31	23, 30	mpbird 167	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴))
32		fveq1 5668	. . . . . . . . . 10 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → (𝑔‘𝑥) = ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥))
33	32	eqeq1d 2241	. . . . . . . . 9 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → ((𝑔‘𝑥) = 1 ↔ ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1))
34	33	ralbidv 2542	. . . . . . . 8 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1))
35	34	dcbid 846	. . . . . . 7 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → (DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 ↔ DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1))
36	35	rspcv 2916	. . . . . 6 ⊢ ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴) → (∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 → DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1))
37	31, 36	syl 14	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 → DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1))
38		eqid 2232	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))
39		fveq2 5669	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑓‘𝑧) = (𝑓‘𝑥))
40	39	oveq2d 6065	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → (1 − (𝑓‘𝑧)) = (1 − (𝑓‘𝑥)))
41		simpr 110	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
42	22	ralrimiva 2615	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑧 ∈ 𝐴 (1 − (𝑓‘𝑧)) ∈ {0, 1})
43	40	eleq1d 2301	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → ((1 − (𝑓‘𝑧)) ∈ {0, 1} ↔ (1 − (𝑓‘𝑥)) ∈ {0, 1}))
44	43	cbvralv 2777	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝐴 (1 − (𝑓‘𝑧)) ∈ {0, 1} ↔ ∀𝑥 ∈ 𝐴 (1 − (𝑓‘𝑥)) ∈ {0, 1})
45	42, 44	sylib 122	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑥 ∈ 𝐴 (1 − (𝑓‘𝑥)) ∈ {0, 1})
46	45	r19.21bi 2630	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (1 − (𝑓‘𝑥)) ∈ {0, 1})
47	38, 40, 41, 46	fvmptd3 5770	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = (1 − (𝑓‘𝑥)))
48	47	eqeq1d 2241	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ (1 − (𝑓‘𝑥)) = 1))
49		1cnd 8289	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 1 ∈ ℂ)
50		0z 9587	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℤ
51		1z 9602	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℤ
52		prssi 3851	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℤ) → {0, 1} ⊆ ℤ)
53	50, 51, 52	mp2an 426	. . . . . . . . . . . 12 ⊢ {0, 1} ⊆ ℤ
54	16	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → 𝑓:𝐴⟶{0, 1})
55	54	ffvelcdmda 5811	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1})
56	53, 55	sselid 3235	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℤ)
57	56	zcnd 9700	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℂ)
58		subsub23 8477	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ (𝑓‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → ((1 − (𝑓‘𝑥)) = 1 ↔ (1 − 1) = (𝑓‘𝑥)))
59	49, 57, 49, 58	syl3anc 1274	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((1 − (𝑓‘𝑥)) = 1 ↔ (1 − 1) = (𝑓‘𝑥)))
60	48, 59	bitrd 188	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ (1 − 1) = (𝑓‘𝑥)))
61	11	eqeq1i 2240	. . . . . . . . 9 ⊢ ((1 − 1) = (𝑓‘𝑥) ↔ 0 = (𝑓‘𝑥))
62		eqcom 2234	. . . . . . . . 9 ⊢ (0 = (𝑓‘𝑥) ↔ (𝑓‘𝑥) = 0)
63	61, 62	bitri 184	. . . . . . . 8 ⊢ ((1 − 1) = (𝑓‘𝑥) ↔ (𝑓‘𝑥) = 0)
64	60, 63	bitrdi 196	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ (𝑓‘𝑥) = 0))
65	64	ralbidva 2538	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
66	65	dcbid 846	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
67	37, 66	sylibd 149	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 → DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
68	67	ralrimdva 2622	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 → ∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
69		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (𝑔‘𝑧) = 0)
70	69	oveq2d 6065	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (1 − (𝑔‘𝑧)) = (1 − 0))
71	70, 4	eqtrdi 2281	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (1 − (𝑔‘𝑧)) = 1)
72	71, 7	eqeltrdi 2323	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (1 − (𝑔‘𝑧)) ∈ {0, 1})
73		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (𝑔‘𝑧) = 1)
74	73	oveq2d 6065	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (1 − (𝑔‘𝑧)) = (1 − 1))
75	74, 11	eqtrdi 2281	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (1 − (𝑔‘𝑧)) = 0)
76	75, 14	eqeltrdi 2323	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (1 − (𝑔‘𝑧)) ∈ {0, 1})
77		elmapi 6903	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ ({0, 1} ↑_𝑚 𝐴) → 𝑔:𝐴⟶{0, 1})
78	77	adantl 277	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → 𝑔:𝐴⟶{0, 1})
79	78	ffvelcdmda 5811	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑔‘𝑧) ∈ {0, 1})
80		elpri 3711	. . . . . . . . . 10 ⊢ ((𝑔‘𝑧) ∈ {0, 1} → ((𝑔‘𝑧) = 0 ∨ (𝑔‘𝑧) = 1))
81	79, 80	syl 14	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → ((𝑔‘𝑧) = 0 ∨ (𝑔‘𝑧) = 1))
82	72, 76, 81	mpjaodan 806	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (1 − (𝑔‘𝑧)) ∈ {0, 1})
83	82	fmpttd 5831	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))):𝐴⟶{0, 1})
84	27	a1i 9	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → {0, 1} ∈ V)
85		simpl 109	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → 𝐴 ∈ 𝑉)
86	84, 85	elmapd 6895	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴) ↔ (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))):𝐴⟶{0, 1}))
87	83, 86	mpbird 167	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴))
88		fveq1 5668	. . . . . . . . . 10 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → (𝑓‘𝑥) = ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥))
89	88	eqeq1d 2241	. . . . . . . . 9 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → ((𝑓‘𝑥) = 0 ↔ ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0))
90	89	ralbidv 2542	. . . . . . . 8 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0))
91	90	dcbid 846	. . . . . . 7 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → (DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ↔ DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0))
92	91	rspcv 2916	. . . . . 6 ⊢ ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴) → (∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 → DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0))
93	87, 92	syl 14	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 → DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0))
94		eqid 2232	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))
95		fveq2 5669	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑔‘𝑧) = (𝑔‘𝑥))
96	95	oveq2d 6065	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → (1 − (𝑔‘𝑧)) = (1 − (𝑔‘𝑥)))
97		simpr 110	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
98	82	ralrimiva 2615	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑧 ∈ 𝐴 (1 − (𝑔‘𝑧)) ∈ {0, 1})
99	96	eleq1d 2301	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → ((1 − (𝑔‘𝑧)) ∈ {0, 1} ↔ (1 − (𝑔‘𝑥)) ∈ {0, 1}))
100	99	cbvralv 2777	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝐴 (1 − (𝑔‘𝑧)) ∈ {0, 1} ↔ ∀𝑥 ∈ 𝐴 (1 − (𝑔‘𝑥)) ∈ {0, 1})
101	98, 100	sylib 122	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑥 ∈ 𝐴 (1 − (𝑔‘𝑥)) ∈ {0, 1})
102	101	r19.21bi 2630	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (1 − (𝑔‘𝑥)) ∈ {0, 1})
103	94, 96, 97, 102	fvmptd3 5770	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = (1 − (𝑔‘𝑥)))
104	103	eqeq1d 2241	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ (1 − (𝑔‘𝑥)) = 0))
105		1cnd 8289	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 1 ∈ ℂ)
106	78	ffvelcdmda 5811	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ {0, 1})
107	53, 106	sselid 3235	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℤ)
108	107	zcnd 9700	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℂ)
109		0cnd 8266	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℂ)
110		subsub23 8477	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ (𝑔‘𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → ((1 − (𝑔‘𝑥)) = 0 ↔ (1 − 0) = (𝑔‘𝑥)))
111	105, 108, 109, 110	syl3anc 1274	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((1 − (𝑔‘𝑥)) = 0 ↔ (1 − 0) = (𝑔‘𝑥)))
112	104, 111	bitrd 188	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ (1 − 0) = (𝑔‘𝑥)))
113	4	eqeq1i 2240	. . . . . . . . 9 ⊢ ((1 − 0) = (𝑔‘𝑥) ↔ 1 = (𝑔‘𝑥))
114		eqcom 2234	. . . . . . . . 9 ⊢ (1 = (𝑔‘𝑥) ↔ (𝑔‘𝑥) = 1)
115	113, 114	bitri 184	. . . . . . . 8 ⊢ ((1 − 0) = (𝑔‘𝑥) ↔ (𝑔‘𝑥) = 1)
116	112, 115	bitrdi 196	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ (𝑔‘𝑥) = 1))
117	116	ralbidva 2538	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
118	117	dcbid 846	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
119	93, 118	sylibd 149	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 → DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
120	119	ralrimdva 2622	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 → ∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
121	68, 120	impbid 129	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 ↔ ∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
122	1, 121	bitrd 188	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 716 DECID wdc 842 = wceq 1398 ∈ wcel 2203 ∀wral 2520 Vcvv 2812 ⊆ wss 3210 {cpr 3689 ↦ cmpt 4170 ⟶wf 5347 ‘cfv 5351 (class class class)co 6049 ↑_𝑚 cmap 6881 WOmnicwomni 7453 ℂcc 8124 0cc0 8126 1c1 8127 − cmin 8443 ℕ₀cn0 9495 ℤcz 9576

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 4224 ax-sep 4227 ax-nul 4235 ax-pow 4286 ax-pr 4321 ax-un 4553 ax-setind 4658 ax-iinf 4709 ax-cnex 8217 ax-resscn 8218 ax-1cn 8219 ax-1re 8220 ax-icn 8221 ax-addcl 8222 ax-addrcl 8223 ax-mulcl 8224 ax-addcom 8226 ax-addass 8228 ax-distr 8230 ax-i2m1 8231 ax-0lt1 8232 ax-0id 8234 ax-rnegex 8235 ax-cnre 8237 ax-pre-ltirr 8238 ax-pre-ltwlin 8239 ax-pre-lttrn 8240 ax-pre-ltadd 8242

This theorem depends on definitions: df-bi 117 df-dc 843 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 2814 df-sbc 3042 df-csb 3138 df-dif 3212 df-un 3214 df-in 3216 df-ss 3223 df-nul 3508 df-pw 3670 df-sn 3694 df-pr 3695 df-op 3697 df-uni 3914 df-int 3949 df-iun 3992 df-br 4109 df-opab 4171 df-mpt 4172 df-tr 4208 df-id 4413 df-iord 4486 df-on 4488 df-ilim 4489 df-suc 4491 df-iom 4712 df-xp 4754 df-rel 4755 df-cnv 4756 df-co 4757 df-dm 4758 df-rn 4759 df-res 4760 df-ima 4761 df-iota 5311 df-fun 5353 df-fn 5354 df-f 5355 df-f1 5356 df-fo 5357 df-f1o 5358 df-fv 5359 df-riota 6002 df-ov 6052 df-oprab 6053 df-mpo 6054 df-recs 6535 df-frec 6621 df-1o 6646 df-2o 6647 df-map 6883 df-womni 7454 df-pnf 8309 df-mnf 8310 df-xr 8311 df-ltxr 8312 df-le 8313 df-sub 8445 df-neg 8446 df-inn 9237 df-n0 9496 df-z 9577 df-uz 9853

This theorem is referenced by: nconstwlpo 16843

W3C validator