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 15695

Description: Weak omniscience stated in terms of equality with 0. Like iswomninn 15694 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 15694	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
2		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (𝑓‘𝑧) = 0)
3	2	oveq2d 5938	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (1 − (𝑓‘𝑧)) = (1 − 0))
4		1m0e1 9103	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
5	3, 4	eqtrdi 2245	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (1 − (𝑓‘𝑧)) = 1)
6		1ex 8021	. . . . . . . . . . 11 ⊢ 1 ∈ V
7	6	prid2 3729	. . . . . . . . . 10 ⊢ 1 ∈ {0, 1}
8	5, 7	eqeltrdi 2287	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (1 − (𝑓‘𝑧)) ∈ {0, 1})
9		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (𝑓‘𝑧) = 1)
10	9	oveq2d 5938	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) = (1 − 1))
11		1m1e0 9059	. . . . . . . . . . 11 ⊢ (1 − 1) = 0
12	10, 11	eqtrdi 2245	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) = 0)
13		c0ex 8020	. . . . . . . . . . 11 ⊢ 0 ∈ V
14	13	prid1 3728	. . . . . . . . . 10 ⊢ 0 ∈ {0, 1}
15	12, 14	eqeltrdi 2287	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) ∈ {0, 1})
16		elmapi 6729	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ ({0, 1} ↑_𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
17	16	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1})
18		simpr 110	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
19	17, 18	ffvelcdmd 5698	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑓‘𝑧) ∈ {0, 1})
20		elpri 3645	. . . . . . . . . 10 ⊢ ((𝑓‘𝑧) ∈ {0, 1} → ((𝑓‘𝑧) = 0 ∨ (𝑓‘𝑧) = 1))
21	19, 20	syl 14	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → ((𝑓‘𝑧) = 0 ∨ (𝑓‘𝑧) = 1))
22	8, 15, 21	mpjaodan 799	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (1 − (𝑓‘𝑧)) ∈ {0, 1})
23	22	fmpttd 5717	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))):𝐴⟶{0, 1})
24		0nn0 9264	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
25		1nn0 9265	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
26		prexg 4244	. . . . . . . . . 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 6721	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴) ↔ (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))):𝐴⟶{0, 1}))
31	23, 30	mpbird 167	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴))
32		fveq1 5557	. . . . . . . . . 10 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → (𝑔‘𝑥) = ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥))
33	32	eqeq1d 2205	. . . . . . . . 9 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → ((𝑔‘𝑥) = 1 ↔ ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1))
34	33	ralbidv 2497	. . . . . . . 8 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1))
35	34	dcbid 839	. . . . . . 7 ⊢ (𝑔 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) → (DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 ↔ DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1))
36	35	rspcv 2864	. . . . . 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 2196	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) = (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))
39		fveq2 5558	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑓‘𝑧) = (𝑓‘𝑥))
40	39	oveq2d 5938	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → (1 − (𝑓‘𝑧)) = (1 − (𝑓‘𝑥)))
41		simpr 110	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
42	22	ralrimiva 2570	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑧 ∈ 𝐴 (1 − (𝑓‘𝑧)) ∈ {0, 1})
43	40	eleq1d 2265	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → ((1 − (𝑓‘𝑧)) ∈ {0, 1} ↔ (1 − (𝑓‘𝑥)) ∈ {0, 1}))
44	43	cbvralv 2729	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝐴 (1 − (𝑓‘𝑧)) ∈ {0, 1} ↔ ∀𝑥 ∈ 𝐴 (1 − (𝑓‘𝑥)) ∈ {0, 1})
45	42, 44	sylib 122	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑥 ∈ 𝐴 (1 − (𝑓‘𝑥)) ∈ {0, 1})
46	45	r19.21bi 2585	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (1 − (𝑓‘𝑥)) ∈ {0, 1})
47	38, 40, 41, 46	fvmptd3 5655	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = (1 − (𝑓‘𝑥)))
48	47	eqeq1d 2205	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ (1 − (𝑓‘𝑥)) = 1))
49		1cnd 8042	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 1 ∈ ℂ)
50		0z 9337	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℤ
51		1z 9352	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℤ
52		prssi 3780	. . . . . . . . . . . . 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 5697	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1})
56	53, 55	sselid 3181	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℤ)
57	56	zcnd 9449	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℂ)
58		subsub23 8231	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ (𝑓‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → ((1 − (𝑓‘𝑥)) = 1 ↔ (1 − 1) = (𝑓‘𝑥)))
59	49, 57, 49, 58	syl3anc 1249	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((1 − (𝑓‘𝑥)) = 1 ↔ (1 − 1) = (𝑓‘𝑥)))
60	48, 59	bitrd 188	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ (1 − 1) = (𝑓‘𝑥)))
61	11	eqeq1i 2204	. . . . . . . . 9 ⊢ ((1 − 1) = (𝑓‘𝑥) ↔ 0 = (𝑓‘𝑥))
62		eqcom 2198	. . . . . . . . 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 2493	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
66	65	dcbid 839	. . . . 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 2577	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1 → ∀𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
69		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (𝑔‘𝑧) = 0)
70	69	oveq2d 5938	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (1 − (𝑔‘𝑧)) = (1 − 0))
71	70, 4	eqtrdi 2245	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (1 − (𝑔‘𝑧)) = 1)
72	71, 7	eqeltrdi 2287	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 0) → (1 − (𝑔‘𝑧)) ∈ {0, 1})
73		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (𝑔‘𝑧) = 1)
74	73	oveq2d 5938	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (1 − (𝑔‘𝑧)) = (1 − 1))
75	74, 11	eqtrdi 2245	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (1 − (𝑔‘𝑧)) = 0)
76	75, 14	eqeltrdi 2287	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑔‘𝑧) = 1) → (1 − (𝑔‘𝑧)) ∈ {0, 1})
77		elmapi 6729	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ ({0, 1} ↑_𝑚 𝐴) → 𝑔:𝐴⟶{0, 1})
78	77	adantl 277	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → 𝑔:𝐴⟶{0, 1})
79	78	ffvelcdmda 5697	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑔‘𝑧) ∈ {0, 1})
80		elpri 3645	. . . . . . . . . 10 ⊢ ((𝑔‘𝑧) ∈ {0, 1} → ((𝑔‘𝑧) = 0 ∨ (𝑔‘𝑧) = 1))
81	79, 80	syl 14	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → ((𝑔‘𝑧) = 0 ∨ (𝑔‘𝑧) = 1))
82	72, 76, 81	mpjaodan 799	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (1 − (𝑔‘𝑧)) ∈ {0, 1})
83	82	fmpttd 5717	. . . . . . 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 6721	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴) ↔ (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))):𝐴⟶{0, 1}))
87	83, 86	mpbird 167	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴))
88		fveq1 5557	. . . . . . . . . 10 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → (𝑓‘𝑥) = ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥))
89	88	eqeq1d 2205	. . . . . . . . 9 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → ((𝑓‘𝑥) = 0 ↔ ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0))
90	89	ralbidv 2497	. . . . . . . 8 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0))
91	90	dcbid 839	. . . . . . 7 ⊢ (𝑓 = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) → (DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ↔ DECID ∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0))
92	91	rspcv 2864	. . . . . 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 2196	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) = (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))
95		fveq2 5558	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑔‘𝑧) = (𝑔‘𝑥))
96	95	oveq2d 5938	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → (1 − (𝑔‘𝑧)) = (1 − (𝑔‘𝑥)))
97		simpr 110	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
98	82	ralrimiva 2570	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑧 ∈ 𝐴 (1 − (𝑔‘𝑧)) ∈ {0, 1})
99	96	eleq1d 2265	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → ((1 − (𝑔‘𝑧)) ∈ {0, 1} ↔ (1 − (𝑔‘𝑥)) ∈ {0, 1}))
100	99	cbvralv 2729	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝐴 (1 − (𝑔‘𝑧)) ∈ {0, 1} ↔ ∀𝑥 ∈ 𝐴 (1 − (𝑔‘𝑥)) ∈ {0, 1})
101	98, 100	sylib 122	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → ∀𝑥 ∈ 𝐴 (1 − (𝑔‘𝑥)) ∈ {0, 1})
102	101	r19.21bi 2585	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (1 − (𝑔‘𝑥)) ∈ {0, 1})
103	94, 96, 97, 102	fvmptd3 5655	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = (1 − (𝑔‘𝑥)))
104	103	eqeq1d 2205	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ (1 − (𝑔‘𝑥)) = 0))
105		1cnd 8042	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 1 ∈ ℂ)
106	78	ffvelcdmda 5697	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ {0, 1})
107	53, 106	sselid 3181	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℤ)
108	107	zcnd 9449	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℂ)
109		0cnd 8019	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℂ)
110		subsub23 8231	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ (𝑔‘𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → ((1 − (𝑔‘𝑥)) = 0 ↔ (1 − 0) = (𝑔‘𝑥)))
111	105, 108, 109, 110	syl3anc 1249	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((1 − (𝑔‘𝑥)) = 0 ↔ (1 − 0) = (𝑔‘𝑥)))
112	104, 111	bitrd 188	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ (1 − 0) = (𝑔‘𝑥)))
113	4	eqeq1i 2204	. . . . . . . . 9 ⊢ ((1 − 0) = (𝑔‘𝑥) ↔ 1 = (𝑔‘𝑥))
114		eqcom 2198	. . . . . . . . 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 2493	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
118	117	dcbid 839	. . . . 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 2577	. . 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 709 DECID wdc 835 = wceq 1364 ∈ wcel 2167 ∀wral 2475 Vcvv 2763 ⊆ wss 3157 {cpr 3623 ↦ cmpt 4094 ⟶wf 5254 ‘cfv 5258 (class class class)co 5922 ↑_𝑚 cmap 6707 WOmnicwomni 7229 ℂcc 7877 0cc0 7879 1c1 7880 − cmin 8197 ℕ₀cn0 9249 ℤcz 9326

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 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-addcom 7979 ax-addass 7981 ax-distr 7983 ax-i2m1 7984 ax-0lt1 7985 ax-0id 7987 ax-rnegex 7988 ax-cnre 7990 ax-pre-ltirr 7991 ax-pre-ltwlin 7992 ax-pre-lttrn 7993 ax-pre-ltadd 7995

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-recs 6363 df-frec 6449 df-1o 6474 df-2o 6475 df-map 6709 df-womni 7230 df-pnf 8063 df-mnf 8064 df-xr 8065 df-ltxr 8066 df-le 8067 df-sub 8199 df-neg 8200 df-inn 8991 df-n0 9250 df-z 9327 df-uz 9602

This theorem is referenced by: nconstwlpo 15710

W3C validator