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 15782

Description: Weak omniscience stated in terms of equality with 0. Like iswomninn 15781 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 15781	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1))
2		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (𝑓‘𝑧) = 0)
3	2	oveq2d 5941	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (1 − (𝑓‘𝑧)) = (1 − 0))
4		1m0e1 9120	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
5	3, 4	eqtrdi 2245	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 0) → (1 − (𝑓‘𝑧)) = 1)
6		1ex 8038	. . . . . . . . . . 11 ⊢ 1 ∈ V
7	6	prid2 3730	. . . . . . . . . 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 5941	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) = (1 − 1))
11		1m1e0 9076	. . . . . . . . . . 11 ⊢ (1 − 1) = 0
12	10, 11	eqtrdi 2245	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) = 0)
13		c0ex 8037	. . . . . . . . . . 11 ⊢ 0 ∈ V
14	13	prid1 3729	. . . . . . . . . 10 ⊢ 0 ∈ {0, 1}
15	12, 14	eqeltrdi 2287	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (𝑓‘𝑧) = 1) → (1 − (𝑓‘𝑧)) ∈ {0, 1})
16		elmapi 6738	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ ({0, 1} ↑_𝑚 𝐴) → 𝑓:𝐴⟶{0, 1})
17	16	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1})
18		simpr 110	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
19	17, 18	ffvelcdmd 5701	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑓‘𝑧) ∈ {0, 1})
20		elpri 3646	. . . . . . . . . 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 5720	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))):𝐴⟶{0, 1})
24		0nn0 9281	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
25		1nn0 9282	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
26		prexg 4245	. . . . . . . . . 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 6730	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴) ↔ (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))):𝐴⟶{0, 1}))
31	23, 30	mpbird 167	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴))
32		fveq1 5560	. . . . . . . . . 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 5561	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑓‘𝑧) = (𝑓‘𝑥))
40	39	oveq2d 5941	. . . . . . . . . . 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 5658	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = (1 − (𝑓‘𝑥)))
48	47	eqeq1d 2205	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑓‘𝑧)))‘𝑥) = 1 ↔ (1 − (𝑓‘𝑥)) = 1))
49		1cnd 8059	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 1 ∈ ℂ)
50		0z 9354	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℤ
51		1z 9369	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℤ
52		prssi 3781	. . . . . . . . . . . . 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 5700	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1})
56	53, 55	sselid 3182	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℤ)
57	56	zcnd 9466	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℂ)
58		subsub23 8248	. . . . . . . . . 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 5941	. . . . . . . . . . 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 5941	. . . . . . . . . . 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 6738	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ ({0, 1} ↑_𝑚 𝐴) → 𝑔:𝐴⟶{0, 1})
78	77	adantl 277	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → 𝑔:𝐴⟶{0, 1})
79	78	ffvelcdmda 5700	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑔‘𝑧) ∈ {0, 1})
80		elpri 3646	. . . . . . . . . 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 5720	. . . . . . 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 6730	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴) ↔ (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))):𝐴⟶{0, 1}))
87	83, 86	mpbird 167	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) → (𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧))) ∈ ({0, 1} ↑_𝑚 𝐴))
88		fveq1 5560	. . . . . . . . . 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 5561	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑔‘𝑧) = (𝑔‘𝑥))
96	95	oveq2d 5941	. . . . . . . . . . 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 5658	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = (1 − (𝑔‘𝑥)))
104	103	eqeq1d 2205	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ (1 − (𝑔‘𝑧)))‘𝑥) = 0 ↔ (1 − (𝑔‘𝑥)) = 0))
105		1cnd 8059	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 1 ∈ ℂ)
106	78	ffvelcdmda 5700	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ {0, 1})
107	53, 106	sselid 3182	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℤ)
108	107	zcnd 9466	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℂ)
109		0cnd 8036	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑_𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℂ)
110		subsub23 8248	. . . . . . . . . 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 3624 ↦ cmpt 4095 ⟶wf 5255 ‘cfv 5259 (class class class)co 5925 ↑_𝑚 cmap 6716 WOmnicwomni 7238 ℂcc 7894 0cc0 7896 1c1 7897 − cmin 8214 ℕ₀cn0 9266 ℤcz 9343

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 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7987 ax-resscn 7988 ax-1cn 7989 ax-1re 7990 ax-icn 7991 ax-addcl 7992 ax-addrcl 7993 ax-mulcl 7994 ax-addcom 7996 ax-addass 7998 ax-distr 8000 ax-i2m1 8001 ax-0lt1 8002 ax-0id 8004 ax-rnegex 8005 ax-cnre 8007 ax-pre-ltirr 8008 ax-pre-ltwlin 8009 ax-pre-lttrn 8010 ax-pre-ltadd 8012

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 3452 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-riota 5880 df-ov 5928 df-oprab 5929 df-mpo 5930 df-recs 6372 df-frec 6458 df-1o 6483 df-2o 6484 df-map 6718 df-womni 7239 df-pnf 8080 df-mnf 8081 df-xr 8082 df-ltxr 8083 df-le 8084 df-sub 8216 df-neg 8217 df-inn 9008 df-n0 9267 df-z 9344 df-uz 9619

This theorem is referenced by: nconstwlpo 15797

W3C validator