gpgprismgr4cycllem3 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > gpgprismgr4cycllem3		Structured version Visualization version GIF version

Theorem gpgprismgr4cycllem3 48486

Description: Lemma 3 for gpgprismgr4cycl0 48495. (Contributed by AV, 5-Nov-2025.)

**Hypothesis**
Ref	Expression
gpgprismgr4cycllem1.f	⊢ 𝐹 = ⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩

**Assertion**
Ref	Expression
gpgprismgr4cycllem3	⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 ∈ (0..^4)) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))

Distinct variable groups: 𝑥,𝑁 𝑥,𝑋 Allowed substitution hint: 𝐹(𝑥)

**Proof of Theorem gpgprismgr4cycllem3**
Step	Hyp	Ref	Expression
1		fzo0to42pr 13683	. . . . 5 ⊢ (0..^4) = ({0, 1} ∪ {2, 3})
2	1	eleq2i 2829	. . . 4 ⊢ (𝑋 ∈ (0..^4) ↔ 𝑋 ∈ ({0, 1} ∪ {2, 3}))
3		elun 4107	. . . 4 ⊢ (𝑋 ∈ ({0, 1} ∪ {2, 3}) ↔ (𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}))
4	2, 3	bitri 275	. . 3 ⊢ (𝑋 ∈ (0..^4) ↔ (𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}))
5		elpri 4606	. . . . 5 ⊢ (𝑋 ∈ {0, 1} → (𝑋 = 0 ∨ 𝑋 = 1))
6		c0ex 11140	. . . . . . . . . . . 12 ⊢ 0 ∈ V
7	6	prid1 4721	. . . . . . . . . . 11 ⊢ 0 ∈ {0, 1}
8	7	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 0 ∈ {0, 1})
9		eluz3nn 12816	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℕ)
10		lbfzo0 13629	. . . . . . . . . . 11 ⊢ (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
11	9, 10	sylibr 234	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 0 ∈ (0..^𝑁))
12	8, 11	opelxpd 5673	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨0, 0⟩ ∈ ({0, 1} × (0..^𝑁)))
13		1nn0 12431	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ₀
14	13	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ ℕ₀)
15		uzuzle23 12811	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ (ℤ_≥‘2))
16		eluz2gt1 12847	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 1 < 𝑁)
17	15, 16	syl 17	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 < 𝑁)
18		elfzo0 13630	. . . . . . . . . . 11 ⊢ (1 ∈ (0..^𝑁) ↔ (1 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 1 < 𝑁))
19	14, 9, 17, 18	syl3anbrc 1345	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ (0..^𝑁))
20	8, 19	opelxpd 5673	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨0, 1⟩ ∈ ({0, 1} × (0..^𝑁)))
21		prelpwi 5404	. . . . . . . . 9 ⊢ ((⟨0, 0⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨0, 1⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
22	12, 20, 21	syl2anc 585	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
23		opeq2 4832	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨0, 𝑥⟩ = ⟨0, 0⟩)
24		oveq1 7377	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1))
25	24	oveq1d 7385	. . . . . . . . . . . . 13 ⊢ (𝑥 = 0 → ((𝑥 + 1) mod 𝑁) = ((0 + 1) mod 𝑁))
26	25	opeq2d 4838	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨0, ((𝑥 + 1) mod 𝑁)⟩ = ⟨0, ((0 + 1) mod 𝑁)⟩)
27	23, 26	preq12d 4700	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩})
28	27	eqeq2d 2748	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
29		opeq2 4832	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨1, 𝑥⟩ = ⟨1, 0⟩)
30	23, 29	preq12d 4700	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} = {⟨0, 0⟩, ⟨1, 0⟩})
31	30	eqeq2d 2748	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
32	25	opeq2d 4838	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨1, ((𝑥 + 1) mod 𝑁)⟩ = ⟨1, ((0 + 1) mod 𝑁)⟩)
33	29, 32	preq12d 4700	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})
34	33	eqeq2d 2748	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩}))
35	28, 31, 34	3orbi123d 1438	. . . . . . . . 9 ⊢ (𝑥 = 0 → (({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}) ↔ ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨1, 0⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})))
36		eluzelre 12776	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℝ)
37		1mod 13837	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 1 < 𝑁) → (1 mod 𝑁) = 1)
38	36, 17, 37	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (1 mod 𝑁) = 1)
39		1e0p1 12663	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
40	39	oveq1i 7380	. . . . . . . . . . . . 13 ⊢ (1 mod 𝑁) = ((0 + 1) mod 𝑁)
41	38, 40	eqtr3di 2787	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 = ((0 + 1) mod 𝑁))
42	41	opeq2d 4838	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨0, 1⟩ = ⟨0, ((0 + 1) mod 𝑁)⟩)
43	42	preq2d 4699	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩})
44	43	3mix1d 1338	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨1, 0⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩}))
45	35, 11, 44	rspcedvdw 3581	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ∃𝑥 ∈ (0..^𝑁)({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
46	22, 45	jca 511	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ({⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
47		fveq2 6844	. . . . . . . . . 10 ⊢ (𝑋 = 0 → (𝐹‘𝑋) = (𝐹‘0))
48		gpgprismgr4cycllem1.f	. . . . . . . . . . . 12 ⊢ 𝐹 = ⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩
49	48	fveq1i 6845	. . . . . . . . . . 11 ⊢ (𝐹‘0) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘0)
50		prex 5386	. . . . . . . . . . . 12 ⊢ {⟨0, 0⟩, ⟨0, 1⟩} ∈ V
51		s4fv0 14832	. . . . . . . . . . . 12 ⊢ ({⟨0, 0⟩, ⟨0, 1⟩} ∈ V → (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘0) = {⟨0, 0⟩, ⟨0, 1⟩})
52	50, 51	ax-mp 5	. . . . . . . . . . 11 ⊢ (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘0) = {⟨0, 0⟩, ⟨0, 1⟩}
53	49, 52	eqtri 2760	. . . . . . . . . 10 ⊢ (𝐹‘0) = {⟨0, 0⟩, ⟨0, 1⟩}
54	47, 53	eqtrdi 2788	. . . . . . . . 9 ⊢ (𝑋 = 0 → (𝐹‘𝑋) = {⟨0, 0⟩, ⟨0, 1⟩})
55	54	eleq1d 2822	. . . . . . . 8 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
56	54	eqeq1d 2739	. . . . . . . . . 10 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
57	54	eqeq1d 2739	. . . . . . . . . 10 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
58	54	eqeq1d 2739	. . . . . . . . . 10 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
59	56, 57, 58	3orbi123d 1438	. . . . . . . . 9 ⊢ (𝑋 = 0 → (((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}) ↔ ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
60	59	rexbidv 3162	. . . . . . . 8 ⊢ (𝑋 = 0 → (∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}) ↔ ∃𝑥 ∈ (0..^𝑁)({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
61	55, 60	anbi12d 633	. . . . . . 7 ⊢ (𝑋 = 0 → (((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})) ↔ ({⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
62	46, 61	imbitrrid 246	. . . . . 6 ⊢ (𝑋 = 0 → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
63		1ex 11142	. . . . . . . . . . . 12 ⊢ 1 ∈ V
64	63	prid2 4722	. . . . . . . . . . 11 ⊢ 1 ∈ {0, 1}
65	64	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ {0, 1})
66	65, 19	opelxpd 5673	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁)))
67		prelpwi 5404	. . . . . . . . 9 ⊢ ((⟨0, 1⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
68	20, 66, 67	syl2anc 585	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
69		opeq2 4832	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨0, 𝑥⟩ = ⟨0, 1⟩)
70		oveq1 7377	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (𝑥 + 1) = (1 + 1))
71	70	oveq1d 7385	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → ((𝑥 + 1) mod 𝑁) = ((1 + 1) mod 𝑁))
72	71	opeq2d 4838	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨0, ((𝑥 + 1) mod 𝑁)⟩ = ⟨0, ((1 + 1) mod 𝑁)⟩)
73	69, 72	preq12d 4700	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} = {⟨0, 1⟩, ⟨0, ((1 + 1) mod 𝑁)⟩})
74	73	eqeq2d 2748	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨0, ((1 + 1) mod 𝑁)⟩}))
75		opeq2 4832	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨1, 𝑥⟩ = ⟨1, 1⟩)
76	69, 75	preq12d 4700	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} = {⟨0, 1⟩, ⟨1, 1⟩})
77	76	eqeq2d 2748	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨1, 1⟩}))
78	71	opeq2d 4838	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨1, ((𝑥 + 1) mod 𝑁)⟩ = ⟨1, ((1 + 1) mod 𝑁)⟩)
79	75, 78	preq12d 4700	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} = {⟨1, 1⟩, ⟨1, ((1 + 1) mod 𝑁)⟩})
80	79	eqeq2d 2748	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 1⟩, ⟨1, ((1 + 1) mod 𝑁)⟩}))
81	74, 77, 80	3orbi123d 1438	. . . . . . . . 9 ⊢ (𝑥 = 1 → (({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}) ↔ ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨0, ((1 + 1) mod 𝑁)⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨1, 1⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 1⟩, ⟨1, ((1 + 1) mod 𝑁)⟩})))
82		eqid 2737	. . . . . . . . . . 11 ⊢ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨1, 1⟩}
83	82	3mix2i 1336	. . . . . . . . . 10 ⊢ ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨0, ((1 + 1) mod 𝑁)⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨1, 1⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 1⟩, ⟨1, ((1 + 1) mod 𝑁)⟩})
84	83	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨0, ((1 + 1) mod 𝑁)⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨1, 1⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 1⟩, ⟨1, ((1 + 1) mod 𝑁)⟩}))
85	81, 19, 84	rspcedvdw 3581	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ∃𝑥 ∈ (0..^𝑁)({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
86	68, 85	jca 511	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ({⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
87		fveq2 6844	. . . . . . . . . 10 ⊢ (𝑋 = 1 → (𝐹‘𝑋) = (𝐹‘1))
88	48	fveq1i 6845	. . . . . . . . . . 11 ⊢ (𝐹‘1) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘1)
89		prex 5386	. . . . . . . . . . . 12 ⊢ {⟨0, 1⟩, ⟨1, 1⟩} ∈ V
90		s4fv1 14833	. . . . . . . . . . . 12 ⊢ ({⟨0, 1⟩, ⟨1, 1⟩} ∈ V → (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘1) = {⟨0, 1⟩, ⟨1, 1⟩})
91	89, 90	ax-mp 5	. . . . . . . . . . 11 ⊢ (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘1) = {⟨0, 1⟩, ⟨1, 1⟩}
92	88, 91	eqtri 2760	. . . . . . . . . 10 ⊢ (𝐹‘1) = {⟨0, 1⟩, ⟨1, 1⟩}
93	87, 92	eqtrdi 2788	. . . . . . . . 9 ⊢ (𝑋 = 1 → (𝐹‘𝑋) = {⟨0, 1⟩, ⟨1, 1⟩})
94	93	eleq1d 2822	. . . . . . . 8 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
95	93	eqeq1d 2739	. . . . . . . . . 10 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
96	93	eqeq1d 2739	. . . . . . . . . 10 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
97	93	eqeq1d 2739	. . . . . . . . . 10 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
98	95, 96, 97	3orbi123d 1438	. . . . . . . . 9 ⊢ (𝑋 = 1 → (((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}) ↔ ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
99	98	rexbidv 3162	. . . . . . . 8 ⊢ (𝑋 = 1 → (∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}) ↔ ∃𝑥 ∈ (0..^𝑁)({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
100	94, 99	anbi12d 633	. . . . . . 7 ⊢ (𝑋 = 1 → (((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})) ↔ ({⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
101	86, 100	imbitrrid 246	. . . . . 6 ⊢ (𝑋 = 1 → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
102	62, 101	jaoi 858	. . . . 5 ⊢ ((𝑋 = 0 ∨ 𝑋 = 1) → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
103	5, 102	syl 17	. . . 4 ⊢ (𝑋 ∈ {0, 1} → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
104		elpri 4606	. . . . 5 ⊢ (𝑋 ∈ {2, 3} → (𝑋 = 2 ∨ 𝑋 = 3))
105	65, 11	opelxpd 5673	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁)))
106	66, 105	jca 511	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁))))
107	106	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 = 2) → (⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁))))
108		prelpwi 5404	. . . . . . . . . 10 ⊢ ((⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨1, 1⟩, ⟨1, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
109	107, 108	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 = 2) → {⟨1, 1⟩, ⟨1, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
110	27	eqeq2d 2748	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
111	30	eqeq2d 2748	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
112	33	eqeq2d 2748	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩}))
113	110, 111, 112	3orbi123d 1438	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → (({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}) ↔ ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})))
114		prcom 4691	. . . . . . . . . . . . 13 ⊢ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 0⟩, ⟨1, 1⟩}
115	41	opeq2d 4838	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨1, 1⟩ = ⟨1, ((0 + 1) mod 𝑁)⟩)
116	115	preq2d 4699	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨1, 0⟩, ⟨1, 1⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})
117	114, 116	eqtrid 2784	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})
118	117	3mix3d 1340	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩}))
119	113, 11, 118	rspcedvdw 3581	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ∃𝑥 ∈ (0..^𝑁)({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
120	119	adantr 480	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 = 2) → ∃𝑥 ∈ (0..^𝑁)({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
121	109, 120	jca 511	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 = 2) → ({⟨1, 1⟩, ⟨1, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
122		fveq2 6844	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → (𝐹‘𝑋) = (𝐹‘2))
123	48	fveq1i 6845	. . . . . . . . . . . . 13 ⊢ (𝐹‘2) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘2)
124		prex 5386	. . . . . . . . . . . . . 14 ⊢ {⟨1, 1⟩, ⟨1, 0⟩} ∈ V
125		s4fv2 14834	. . . . . . . . . . . . . 14 ⊢ ({⟨1, 1⟩, ⟨1, 0⟩} ∈ V → (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘2) = {⟨1, 1⟩, ⟨1, 0⟩})
126	124, 125	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘2) = {⟨1, 1⟩, ⟨1, 0⟩}
127	123, 126	eqtri 2760	. . . . . . . . . . . 12 ⊢ (𝐹‘2) = {⟨1, 1⟩, ⟨1, 0⟩}
128	122, 127	eqtrdi 2788	. . . . . . . . . . 11 ⊢ (𝑋 = 2 → (𝐹‘𝑋) = {⟨1, 1⟩, ⟨1, 0⟩})
129	128	eleq1d 2822	. . . . . . . . . 10 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨1, 1⟩, ⟨1, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
130	128	eqeq1d 2739	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
131	128	eqeq1d 2739	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
132	128	eqeq1d 2739	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
133	130, 131, 132	3orbi123d 1438	. . . . . . . . . . 11 ⊢ (𝑋 = 2 → (((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}) ↔ ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
134	133	rexbidv 3162	. . . . . . . . . 10 ⊢ (𝑋 = 2 → (∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}) ↔ ∃𝑥 ∈ (0..^𝑁)({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
135	129, 134	anbi12d 633	. . . . . . . . 9 ⊢ (𝑋 = 2 → (((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})) ↔ ({⟨1, 1⟩, ⟨1, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
136	135	adantl 481	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 = 2) → (((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})) ↔ ({⟨1, 1⟩, ⟨1, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
137	121, 136	mpbird 257	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 = 2) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
138	137	expcom 413	. . . . . 6 ⊢ (𝑋 = 2 → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
139		prelpwi 5404	. . . . . . . . 9 ⊢ ((⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨0, 0⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
140	105, 12, 139	syl2anc 585	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
141	27	eqeq2d 2748	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
142	30	eqeq2d 2748	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
143	33	eqeq2d 2748	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩}))
144	141, 142, 143	3orbi123d 1438	. . . . . . . . 9 ⊢ (𝑥 = 0 → (({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}) ↔ ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})))
145		prcom 4691	. . . . . . . . . . 11 ⊢ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩}
146	145	3mix2i 1336	. . . . . . . . . 10 ⊢ ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})
147	146	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩}))
148	144, 11, 147	rspcedvdw 3581	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ∃𝑥 ∈ (0..^𝑁)({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
149	140, 148	jca 511	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ({⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
150		fveq2 6844	. . . . . . . . . 10 ⊢ (𝑋 = 3 → (𝐹‘𝑋) = (𝐹‘3))
151	48	fveq1i 6845	. . . . . . . . . . 11 ⊢ (𝐹‘3) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘3)
152		prex 5386	. . . . . . . . . . . 12 ⊢ {⟨1, 0⟩, ⟨0, 0⟩} ∈ V
153		s4fv3 14835	. . . . . . . . . . . 12 ⊢ ({⟨1, 0⟩, ⟨0, 0⟩} ∈ V → (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘3) = {⟨1, 0⟩, ⟨0, 0⟩})
154	152, 153	ax-mp 5	. . . . . . . . . . 11 ⊢ (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘3) = {⟨1, 0⟩, ⟨0, 0⟩}
155	151, 154	eqtri 2760	. . . . . . . . . 10 ⊢ (𝐹‘3) = {⟨1, 0⟩, ⟨0, 0⟩}
156	150, 155	eqtrdi 2788	. . . . . . . . 9 ⊢ (𝑋 = 3 → (𝐹‘𝑋) = {⟨1, 0⟩, ⟨0, 0⟩})
157	156	eleq1d 2822	. . . . . . . 8 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
158	156	eqeq1d 2739	. . . . . . . . . 10 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
159	156	eqeq1d 2739	. . . . . . . . . 10 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
160	156	eqeq1d 2739	. . . . . . . . . 10 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
161	158, 159, 160	3orbi123d 1438	. . . . . . . . 9 ⊢ (𝑋 = 3 → (((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}) ↔ ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
162	161	rexbidv 3162	. . . . . . . 8 ⊢ (𝑋 = 3 → (∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}) ↔ ∃𝑥 ∈ (0..^𝑁)({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
163	157, 162	anbi12d 633	. . . . . . 7 ⊢ (𝑋 = 3 → (((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})) ↔ ({⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
164	149, 163	imbitrrid 246	. . . . . 6 ⊢ (𝑋 = 3 → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
165	138, 164	jaoi 858	. . . . 5 ⊢ ((𝑋 = 2 ∨ 𝑋 = 3) → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
166	104, 165	syl 17	. . . 4 ⊢ (𝑋 ∈ {2, 3} → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
167	103, 166	jaoi 858	. . 3 ⊢ ((𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}) → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
168	4, 167	sylbi 217	. 2 ⊢ (𝑋 ∈ (0..^4) → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
169	168	impcom 407	1 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 ∈ (0..^4)) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∨ w3o 1086 = wceq 1542 ∈ wcel 2114 ∃wrex 3062 Vcvv 3442 ∪ cun 3901 𝒫 cpw 4556 {cpr 4584 ⟨cop 4588 class class class wbr 5100 × cxp 5632 ‘cfv 6502 (class class class)co 7370 ℝcr 11039 0cc0 11040 1c1 11041 + caddc 11043 < clt 11180 ℕcn 12159 2c2 12214 3c3 12215 4c4 12216 ℕ₀cn0 12415 ℤ_≥cuz 12765 ..^cfzo 13584 mod cmo 13803 ⟨“cs4 14780

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5314 ax-pr 5381 ax-un 7692 ax-cnex 11096 ax-resscn 11097 ax-1cn 11098 ax-icn 11099 ax-addcl 11100 ax-addrcl 11101 ax-mulcl 11102 ax-mulrcl 11103 ax-mulcom 11104 ax-addass 11105 ax-mulass 11106 ax-distr 11107 ax-i2m1 11108 ax-1ne0 11109 ax-1rid 11110 ax-rnegex 11111 ax-rrecex 11112 ax-cnre 11113 ax-pre-lttri 11114 ax-pre-lttrn 11115 ax-pre-ltadd 11116 ax-pre-mulgt0 11117 ax-pre-sup 11118

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5529 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5587 df-we 5589 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6269 df-ord 6330 df-on 6331 df-lim 6332 df-suc 6333 df-iota 6458 df-fun 6504 df-fn 6505 df-f 6506 df-f1 6507 df-fo 6508 df-f1o 6509 df-fv 6510 df-riota 7327 df-ov 7373 df-oprab 7374 df-mpo 7375 df-om 7821 df-1st 7945 df-2nd 7946 df-frecs 8235 df-wrecs 8266 df-recs 8315 df-rdg 8353 df-1o 8409 df-er 8647 df-en 8898 df-dom 8899 df-sdom 8900 df-fin 8901 df-sup 9359 df-inf 9360 df-card 9865 df-pnf 11182 df-mnf 11183 df-xr 11184 df-ltxr 11185 df-le 11186 df-sub 11380 df-neg 11381 df-div 11809 df-nn 12160 df-2 12222 df-3 12223 df-4 12224 df-n0 12416 df-z 12503 df-uz 12766 df-rp 12920 df-fz 13438 df-fzo 13585 df-fl 13726 df-mod 13804 df-hash 14268 df-word 14451 df-concat 14508 df-s1 14534 df-s2 14785 df-s3 14786 df-s4 14787

This theorem is referenced by: gpgprismgr4cycllem10 48493

W3C validator