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 13930

Description: Weak omniscience stated in terms of equality with 0. Like iswomninn 13929 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 13929	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
2		simpr 109	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (𝑓‘𝑧) = 0)
3	2	oveq2d 5858	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (1 − (𝑓‘𝑧)) = (1 − 0))
4		1m0e1 8970	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
5	3, 4	eqtrdi 2215	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (1 − (𝑓‘𝑧)) = 1)
6		1ex 7894	. . . . . . . . . . 11 ⊢ 1 ∈ V
7	6	prid2 3683	. . . . . . . . . 10 ⊢ 1 ∈ {0, 1}
8	5, 7	eqeltrdi 2257	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (1 − (𝑓‘𝑧)) ∈ {0, 1})
9		simpr 109	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (𝑓‘𝑧) = 1)
10	9	oveq2d 5858	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) = (1 − 1))
11		1m1e0 8926	. . . . . . . . . . 11 ⊢ (1 − 1) = 0
12	10, 11	eqtrdi 2215	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) = 0)
13		c0ex 7893	. . . . . . . . . . 11 ⊢ 0 ∈ V
14	13	prid1 3682	. . . . . . . . . 10 ⊢ 0 ∈ {0, 1}
15	12, 14	eqeltrdi 2257	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) ∈ {0, 1})
16		elmapi 6636	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ ({0, 1} ↑_𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
17	16	ad2antlr 481	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1})
18		simpr 109	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
19	17, 18	ffvelrnd 5621	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑓‘𝑧) ∈ {0, 1})
20		elpri 3599	. . . . . . . . . 10 ⊢ ((𝑓‘𝑧) ∈ {0, 1} → ((𝑓‘𝑧) = 0 ∨ (𝑓‘𝑧) = 1))
21	19, 20	syl 14	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → ((𝑓‘𝑧) = 0 ∨ (𝑓‘𝑧) = 1))
22	8, 15, 21	mpjaodan 788	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (1 − (𝑓‘𝑧)) ∈ {0, 1})
23	22	fmpttd 5640	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))):𝐴⟶{0, 1})
24		0nn0 9129	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
25		1nn0 9130	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
26		prexg 4189	. . . . . . . . . 10 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) → {0, 1} ∈ V)
27	24, 25, 26	mp2an 423	. . . . . . . . 9 ⊢ {0, 1} ∈ V
28	27	a1i 9	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → {0, 1} ∈ V)
29		simpl 108	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → 𝐴 ∈ 𝑉)
30	28, 29	elmapd 6628	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴) ↔ (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))):𝐴⟶{0, 1}))
31	23, 30	mpbird 166	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴))
32		fveq1 5485	. . . . . . . . . 10 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → (𝑔‘𝑥) = ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥))
33	32	eqeq1d 2174	. . . . . . . . 9 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → ((𝑔‘𝑥) = 1 ↔ ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1))
34	33	ralbidv 2466	. . . . . . . 8 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1))
35	34	dcbid 828	. . . . . . 7 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → (DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 ↔ DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1))
36	35	rspcv 2826	. . . . . 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 2165	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))
39		fveq2 5486	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑓‘𝑧) = (𝑓‘𝑥))
40	39	oveq2d 5858	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → (1 − (𝑓‘𝑧)) = (1 − (𝑓‘𝑥)))
41		simpr 109	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
42	22	ralrimiva 2539	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑧 ∈ 𝐴 (1 − (𝑓‘𝑧)) ∈ {0, 1})
43	40	eleq1d 2235	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → ((1 − (𝑓‘𝑧)) ∈ {0, 1} ↔ (1 − (𝑓‘𝑥)) ∈ {0, 1}))
44	43	cbvralv 2692	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝐴 (1 − (𝑓‘𝑧)) ∈ {0, 1} ↔ ∀𝑥 ∈ 𝐴 (1 − (𝑓‘𝑥)) ∈ {0, 1})
45	42, 44	sylib 121	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑥 ∈ 𝐴 (1 − (𝑓‘𝑥)) ∈ {0, 1})
46	45	r19.21bi 2554	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (1 − (𝑓‘𝑥)) ∈ {0, 1})
47	38, 40, 41, 46	fvmptd3 5579	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = (1 − (𝑓‘𝑥)))
48	47	eqeq1d 2174	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ (1 − (𝑓‘𝑥)) = 1))
49		1cnd 7915	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 1 ∈ ℂ)
50		0z 9202	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℤ
51		1z 9217	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℤ
52		prssi 3731	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℤ) → {0, 1} ⊆ ℤ)
53	50, 51, 52	mp2an 423	. . . . . . . . . . . 12 ⊢ {0, 1} ⊆ ℤ
54	16	adantl 275	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → 𝑓:𝐴⟶{0, 1})
55	54	ffvelrnda 5620	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1})
56	53, 55	sselid 3140	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℤ)
57	56	zcnd 9314	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℂ)
58		subsub23 8103	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ (𝑓‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → ((1 − (𝑓‘𝑥)) = 1 ↔ (1 − 1) = (𝑓‘𝑥)))
59	49, 57, 49, 58	syl3anc 1228	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((1 − (𝑓‘𝑥)) = 1 ↔ (1 − 1) = (𝑓‘𝑥)))
60	48, 59	bitrd 187	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ (1 − 1) = (𝑓‘𝑥)))
61	11	eqeq1i 2173	. . . . . . . . 9 ⊢ ((1 − 1) = (𝑓‘𝑥) ↔ 0 = (𝑓‘𝑥))
62		eqcom 2167	. . . . . . . . 9 ⊢ (0 = (𝑓‘𝑥) ↔ (𝑓‘𝑥) = 0)
63	61, 62	bitri 183	. . . . . . . 8 ⊢ ((1 − 1) = (𝑓‘𝑥) ↔ (𝑓‘𝑥) = 0)
64	60, 63	bitrdi 195	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ (𝑓‘𝑥) = 0))
65	64	ralbidva 2462	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
66	65	dcbid 828	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
67	37, 66	sylibd 148	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 → DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
68	67	ralrimdva 2546	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 → ∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
69		simpr 109	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (𝑔‘𝑧) = 0)
70	69	oveq2d 5858	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (1 − (𝑔‘𝑧)) = (1 − 0))
71	70, 4	eqtrdi 2215	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (1 − (𝑔‘𝑧)) = 1)
72	71, 7	eqeltrdi 2257	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (1 − (𝑔‘𝑧)) ∈ {0, 1})
73		simpr 109	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (𝑔‘𝑧) = 1)
74	73	oveq2d 5858	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (1 − (𝑔‘𝑧)) = (1 − 1))
75	74, 11	eqtrdi 2215	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (1 − (𝑔‘𝑧)) = 0)
76	75, 14	eqeltrdi 2257	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (1 − (𝑔‘𝑧)) ∈ {0, 1})
77		elmapi 6636	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ ({0, 1} ↑_𝑚 𝐴) → 𝑔:𝐴⟶{0, 1})
78	77	adantl 275	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → 𝑔:𝐴⟶{0, 1})
79	78	ffvelrnda 5620	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑔‘𝑧) ∈ {0, 1})
80		elpri 3599	. . . . . . . . . 10 ⊢ ((𝑔‘𝑧) ∈ {0, 1} → ((𝑔‘𝑧) = 0 ∨ (𝑔‘𝑧) = 1))
81	79, 80	syl 14	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → ((𝑔‘𝑧) = 0 ∨ (𝑔‘𝑧) = 1))
82	72, 76, 81	mpjaodan 788	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (1 − (𝑔‘𝑧)) ∈ {0, 1})
83	82	fmpttd 5640	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))):𝐴⟶{0, 1})
84	27	a1i 9	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → {0, 1} ∈ V)
85		simpl 108	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → 𝐴 ∈ 𝑉)
86	84, 85	elmapd 6628	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴) ↔ (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))):𝐴⟶{0, 1}))
87	83, 86	mpbird 166	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴))
88		fveq1 5485	. . . . . . . . . 10 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → (𝑓‘𝑥) = ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥))
89	88	eqeq1d 2174	. . . . . . . . 9 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → ((𝑓‘𝑥) = 0 ↔ ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0))
90	89	ralbidv 2466	. . . . . . . 8 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0))
91	90	dcbid 828	. . . . . . 7 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → (DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ↔ DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0))
92	91	rspcv 2826	. . . . . 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 2165	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))
95		fveq2 5486	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑔‘𝑧) = (𝑔‘𝑥))
96	95	oveq2d 5858	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → (1 − (𝑔‘𝑧)) = (1 − (𝑔‘𝑥)))
97		simpr 109	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
98	82	ralrimiva 2539	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑧 ∈ 𝐴 (1 − (𝑔‘𝑧)) ∈ {0, 1})
99	96	eleq1d 2235	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → ((1 − (𝑔‘𝑧)) ∈ {0, 1} ↔ (1 − (𝑔‘𝑥)) ∈ {0, 1}))
100	99	cbvralv 2692	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝐴 (1 − (𝑔‘𝑧)) ∈ {0, 1} ↔ ∀𝑥 ∈ 𝐴 (1 − (𝑔‘𝑥)) ∈ {0, 1})
101	98, 100	sylib 121	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑥 ∈ 𝐴 (1 − (𝑔‘𝑥)) ∈ {0, 1})
102	101	r19.21bi 2554	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (1 − (𝑔‘𝑥)) ∈ {0, 1})
103	94, 96, 97, 102	fvmptd3 5579	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = (1 − (𝑔‘𝑥)))
104	103	eqeq1d 2174	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ (1 − (𝑔‘𝑥)) = 0))
105		1cnd 7915	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 1 ∈ ℂ)
106	78	ffvelrnda 5620	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ {0, 1})
107	53, 106	sselid 3140	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℤ)
108	107	zcnd 9314	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℂ)
109		0cnd 7892	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℂ)
110		subsub23 8103	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ (𝑔‘𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → ((1 − (𝑔‘𝑥)) = 0 ↔ (1 − 0) = (𝑔‘𝑥)))
111	105, 108, 109, 110	syl3anc 1228	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((1 − (𝑔‘𝑥)) = 0 ↔ (1 − 0) = (𝑔‘𝑥)))
112	104, 111	bitrd 187	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ (1 − 0) = (𝑔‘𝑥)))
113	4	eqeq1i 2173	. . . . . . . . 9 ⊢ ((1 − 0) = (𝑔‘𝑥) ↔ 1 = (𝑔‘𝑥))
114		eqcom 2167	. . . . . . . . 9 ⊢ (1 = (𝑔‘𝑥) ↔ (𝑔‘𝑥) = 1)
115	113, 114	bitri 183	. . . . . . . 8 ⊢ ((1 − 0) = (𝑔‘𝑥) ↔ (𝑔‘𝑥) = 1)
116	112, 115	bitrdi 195	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ (𝑔‘𝑥) = 1))
117	116	ralbidva 2462	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
118	117	dcbid 828	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
119	93, 118	sylibd 148	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 → DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
120	119	ralrimdva 2546	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 → ∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
121	68, 120	impbid 128	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 ↔ ∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
122	1, 121	bitrd 187	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 698 DECID wdc 824 = wceq 1343 ∈ wcel 2136 ∀wral 2444 Vcvv 2726 ⊆ wss 3116 {cpr 3577 ↦ cmpt 4043 ⟶wf 5184 ‘cfv 5188 (class class class)co 5842 ↑_𝑚 cmap 6614 WOmnicwomni 7127 ℂcc 7751 0cc0 7753 1c1 7754 − cmin 8069 ℕ₀cn0 9114 ℤcz 9191

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 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-addcom 7853 ax-addass 7855 ax-distr 7857 ax-i2m1 7858 ax-0lt1 7859 ax-0id 7861 ax-rnegex 7862 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltwlin 7866 ax-pre-lttrn 7867 ax-pre-ltadd 7869

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-iord 4344 df-on 4346 df-ilim 4347 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-recs 6273 df-frec 6359 df-1o 6384 df-2o 6385 df-map 6616 df-womni 7128 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-le 7939 df-sub 8071 df-neg 8072 df-inn 8858 df-n0 9115 df-z 9192 df-uz 9467

This theorem is referenced by: nconstwlpo 13944

W3C validator