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 13571

Description: Weak omniscience stated in terms of equality with 0. Like iswomninn 13570 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 13570	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
2		simpr 109	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (𝑓‘𝑧) = 0)
3	2	oveq2d 5830	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (1 − (𝑓‘𝑧)) = (1 − 0))
4		1m0e1 8925	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
5	3, 4	eqtrdi 2203	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (1 − (𝑓‘𝑧)) = 1)
6		1ex 7852	. . . . . . . . . . 11 ⊢ 1 ∈ V
7	6	prid2 3662	. . . . . . . . . 10 ⊢ 1 ∈ {0, 1}
8	5, 7	eqeltrdi 2245	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (1 − (𝑓‘𝑧)) ∈ {0, 1})
9		simpr 109	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (𝑓‘𝑧) = 1)
10	9	oveq2d 5830	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) = (1 − 1))
11		1m1e0 8881	. . . . . . . . . . 11 ⊢ (1 − 1) = 0
12	10, 11	eqtrdi 2203	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) = 0)
13		c0ex 7851	. . . . . . . . . . 11 ⊢ 0 ∈ V
14	13	prid1 3661	. . . . . . . . . 10 ⊢ 0 ∈ {0, 1}
15	12, 14	eqeltrdi 2245	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) ∈ {0, 1})
16		elmapi 6604	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ ({0, 1} ↑_𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
17	16	ad2antlr 481	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1})
18		simpr 109	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
19	17, 18	ffvelrnd 5596	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑓‘𝑧) ∈ {0, 1})
20		elpri 3579	. . . . . . . . . 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 5615	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))):𝐴⟶{0, 1})
24		0nn0 9084	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
25		1nn0 9085	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
26		prexg 4166	. . . . . . . . . 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 6596	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴) ↔ (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))):𝐴⟶{0, 1}))
31	23, 30	mpbird 166	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴))
32		fveq1 5460	. . . . . . . . . 10 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → (𝑔‘𝑥) = ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥))
33	32	eqeq1d 2163	. . . . . . . . 9 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → ((𝑔‘𝑥) = 1 ↔ ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1))
34	33	ralbidv 2454	. . . . . . . 8 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1))
35	34	dcbid 824	. . . . . . 7 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → (DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 ↔ DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1))
36	35	rspcv 2809	. . . . . 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 2154	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))
39		fveq2 5461	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑓‘𝑧) = (𝑓‘𝑥))
40	39	oveq2d 5830	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → (1 − (𝑓‘𝑧)) = (1 − (𝑓‘𝑥)))
41		simpr 109	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
42	22	ralrimiva 2527	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑧 ∈ 𝐴 (1 − (𝑓‘𝑧)) ∈ {0, 1})
43	40	eleq1d 2223	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → ((1 − (𝑓‘𝑧)) ∈ {0, 1} ↔ (1 − (𝑓‘𝑥)) ∈ {0, 1}))
44	43	cbvralv 2677	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝐴 (1 − (𝑓‘𝑧)) ∈ {0, 1} ↔ ∀𝑥 ∈ 𝐴 (1 − (𝑓‘𝑥)) ∈ {0, 1})
45	42, 44	sylib 121	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑥 ∈ 𝐴 (1 − (𝑓‘𝑥)) ∈ {0, 1})
46	45	r19.21bi 2542	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (1 − (𝑓‘𝑥)) ∈ {0, 1})
47	38, 40, 41, 46	fvmptd3 5554	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = (1 − (𝑓‘𝑥)))
48	47	eqeq1d 2163	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ (1 − (𝑓‘𝑥)) = 1))
49		1cnd 7873	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 1 ∈ ℂ)
50		0z 9157	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℤ
51		1z 9172	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℤ
52		prssi 3710	. . . . . . . . . . . . 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 5595	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1})
56	53, 55	sseldi 3122	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℤ)
57	56	zcnd 9266	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℂ)
58		subsub23 8059	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ (𝑓‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → ((1 − (𝑓‘𝑥)) = 1 ↔ (1 − 1) = (𝑓‘𝑥)))
59	49, 57, 49, 58	syl3anc 1217	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((1 − (𝑓‘𝑥)) = 1 ↔ (1 − 1) = (𝑓‘𝑥)))
60	48, 59	bitrd 187	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ (1 − 1) = (𝑓‘𝑥)))
61	11	eqeq1i 2162	. . . . . . . . 9 ⊢ ((1 − 1) = (𝑓‘𝑥) ↔ 0 = (𝑓‘𝑥))
62		eqcom 2156	. . . . . . . . 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 2450	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
66	65	dcbid 824	. . . . 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 2534	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 → ∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
69		simpr 109	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (𝑔‘𝑧) = 0)
70	69	oveq2d 5830	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (1 − (𝑔‘𝑧)) = (1 − 0))
71	70, 4	eqtrdi 2203	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (1 − (𝑔‘𝑧)) = 1)
72	71, 7	eqeltrdi 2245	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (1 − (𝑔‘𝑧)) ∈ {0, 1})
73		simpr 109	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (𝑔‘𝑧) = 1)
74	73	oveq2d 5830	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (1 − (𝑔‘𝑧)) = (1 − 1))
75	74, 11	eqtrdi 2203	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (1 − (𝑔‘𝑧)) = 0)
76	75, 14	eqeltrdi 2245	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (1 − (𝑔‘𝑧)) ∈ {0, 1})
77		elmapi 6604	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ ({0, 1} ↑_𝑚 𝐴) → 𝑔:𝐴⟶{0, 1})
78	77	adantl 275	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → 𝑔:𝐴⟶{0, 1})
79	78	ffvelrnda 5595	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑔‘𝑧) ∈ {0, 1})
80		elpri 3579	. . . . . . . . . 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 5615	. . . . . . 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 6596	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴) ↔ (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))):𝐴⟶{0, 1}))
87	83, 86	mpbird 166	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴))
88		fveq1 5460	. . . . . . . . . 10 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → (𝑓‘𝑥) = ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥))
89	88	eqeq1d 2163	. . . . . . . . 9 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → ((𝑓‘𝑥) = 0 ↔ ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0))
90	89	ralbidv 2454	. . . . . . . 8 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0))
91	90	dcbid 824	. . . . . . 7 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → (DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ↔ DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0))
92	91	rspcv 2809	. . . . . 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 2154	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))
95		fveq2 5461	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑔‘𝑧) = (𝑔‘𝑥))
96	95	oveq2d 5830	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → (1 − (𝑔‘𝑧)) = (1 − (𝑔‘𝑥)))
97		simpr 109	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
98	82	ralrimiva 2527	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑧 ∈ 𝐴 (1 − (𝑔‘𝑧)) ∈ {0, 1})
99	96	eleq1d 2223	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → ((1 − (𝑔‘𝑧)) ∈ {0, 1} ↔ (1 − (𝑔‘𝑥)) ∈ {0, 1}))
100	99	cbvralv 2677	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝐴 (1 − (𝑔‘𝑧)) ∈ {0, 1} ↔ ∀𝑥 ∈ 𝐴 (1 − (𝑔‘𝑥)) ∈ {0, 1})
101	98, 100	sylib 121	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑥 ∈ 𝐴 (1 − (𝑔‘𝑥)) ∈ {0, 1})
102	101	r19.21bi 2542	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (1 − (𝑔‘𝑥)) ∈ {0, 1})
103	94, 96, 97, 102	fvmptd3 5554	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = (1 − (𝑔‘𝑥)))
104	103	eqeq1d 2163	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ (1 − (𝑔‘𝑥)) = 0))
105		1cnd 7873	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 1 ∈ ℂ)
106	78	ffvelrnda 5595	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ {0, 1})
107	53, 106	sseldi 3122	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℤ)
108	107	zcnd 9266	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℂ)
109		0cnd 7850	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℂ)
110		subsub23 8059	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ (𝑔‘𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → ((1 − (𝑔‘𝑥)) = 0 ↔ (1 − 0) = (𝑔‘𝑥)))
111	105, 108, 109, 110	syl3anc 1217	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((1 − (𝑔‘𝑥)) = 0 ↔ (1 − 0) = (𝑔‘𝑥)))
112	104, 111	bitrd 187	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ (1 − 0) = (𝑔‘𝑥)))
113	4	eqeq1i 2162	. . . . . . . . 9 ⊢ ((1 − 0) = (𝑔‘𝑥) ↔ 1 = (𝑔‘𝑥))
114		eqcom 2156	. . . . . . . . 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 2450	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
118	117	dcbid 824	. . . . 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 2534	. . 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 820 = wceq 1332 ∈ wcel 2125 ∀wral 2432 Vcvv 2709 ⊆ wss 3098 {cpr 3557 ↦ cmpt 4021 ⟶wf 5159 ‘cfv 5163 (class class class)co 5814 ↑_𝑚 cmap 6582 WOmnicwomni 7085 ℂcc 7709 0cc0 7711 1c1 7712 − cmin 8025 ℕ₀cn0 9069 ℤcz 9146

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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-13 2127 ax-14 2128 ax-ext 2136 ax-coll 4075 ax-sep 4078 ax-nul 4086 ax-pow 4130 ax-pr 4164 ax-un 4388 ax-setind 4490 ax-iinf 4541 ax-cnex 7802 ax-resscn 7803 ax-1cn 7804 ax-1re 7805 ax-icn 7806 ax-addcl 7807 ax-addrcl 7808 ax-mulcl 7809 ax-addcom 7811 ax-addass 7813 ax-distr 7815 ax-i2m1 7816 ax-0lt1 7817 ax-0id 7819 ax-rnegex 7820 ax-cnre 7822 ax-pre-ltirr 7823 ax-pre-ltwlin 7824 ax-pre-lttrn 7825 ax-pre-ltadd 7827

This theorem depends on definitions: df-bi 116 df-dc 821 df-3or 964 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1740 df-eu 2006 df-mo 2007 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ne 2325 df-nel 2420 df-ral 2437 df-rex 2438 df-reu 2439 df-rab 2441 df-v 2711 df-sbc 2934 df-csb 3028 df-dif 3100 df-un 3102 df-in 3104 df-ss 3111 df-nul 3391 df-pw 3541 df-sn 3562 df-pr 3563 df-op 3565 df-uni 3769 df-int 3804 df-iun 3847 df-br 3962 df-opab 4022 df-mpt 4023 df-tr 4059 df-id 4248 df-iord 4321 df-on 4323 df-ilim 4324 df-suc 4326 df-iom 4544 df-xp 4585 df-rel 4586 df-cnv 4587 df-co 4588 df-dm 4589 df-rn 4590 df-res 4591 df-ima 4592 df-iota 5128 df-fun 5165 df-fn 5166 df-f 5167 df-f1 5168 df-fo 5169 df-f1o 5170 df-fv 5171 df-riota 5770 df-ov 5817 df-oprab 5818 df-mpo 5819 df-recs 6242 df-frec 6328 df-1o 6353 df-2o 6354 df-map 6584 df-womni 7086 df-pnf 7893 df-mnf 7894 df-xr 7895 df-ltxr 7896 df-le 7897 df-sub 8027 df-neg 8028 df-inn 8813 df-n0 9070 df-z 9147 df-uz 9419

This theorem is referenced by: nconstwlpo 13585

W3C validator