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 49340

Description: Lemma 3 for gpgprismgr4cycl0 49349. (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 13901	. . . . 5 ⊢ (0..^4) = ({0, 1} ∪ {2, 3})
2	1	eleq2i 2856	. . . 4 ⊢ (𝑋 ∈ (0..^4) ↔ 𝑋 ∈ ({0, 1} ∪ {2, 3}))
3		elun 4155	. . . 4 ⊢ (𝑋 ∈ ({0, 1} ∪ {2, 3}) ↔ (𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}))
4	2, 3	bitri 278	. . 3 ⊢ (𝑋 ∈ (0..^4) ↔ (𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}))
5		elpri 4608	. . . . 5 ⊢ (𝑋 ∈ {0, 1} → (𝑋 = 0 ∨ 𝑋 = 1))
6		0elpr01 11314	. . . . . . . . . . 11 ⊢ 0 ∈ {0, 1}
7	6	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 0 ∈ {0, 1})
8		eluz3nn 13029	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℕ)
9		lbfzo0 13847	. . . . . . . . . . 11 ⊢ (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
10	8, 9	sylibr 237	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 0 ∈ (0..^𝑁))
11	7, 10	opelxpd 5694	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨0, 0⟩ ∈ ({0, 1} × (0..^𝑁)))
12		1nn0 12635	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ₀
13	12	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ ℕ₀)
14		uzuzle23 13024	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ (ℤ_≥‘2))
15		eluz2gt1 13060	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 1 < 𝑁)
16	14, 15	syl 18	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 < 𝑁)
17		elfzo0 13848	. . . . . . . . . . 11 ⊢ (1 ∈ (0..^𝑁) ↔ (1 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 1 < 𝑁))
18	13, 8, 16, 17	syl3anbrc 1362	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ (0..^𝑁))
19	7, 18	opelxpd 5694	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨0, 1⟩ ∈ ({0, 1} × (0..^𝑁)))
20		prelpwi 5419	. . . . . . . . 9 ⊢ ((⟨0, 0⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨0, 1⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
21	11, 19, 20	syl2anc 596	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
22		opeq2 4844	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨0, 𝑥⟩ = ⟨0, 0⟩)
23		oveq1 7437	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1))
24	23	oveq1d 7445	. . . . . . . . . . . . 13 ⊢ (𝑥 = 0 → ((𝑥 + 1) mod 𝑁) = ((0 + 1) mod 𝑁))
25	24	opeq2d 4850	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨0, ((𝑥 + 1) mod 𝑁)⟩ = ⟨0, ((0 + 1) mod 𝑁)⟩)
26	22, 25	preq12d 4702	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩})
27	26	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
28		opeq2 4844	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨1, 𝑥⟩ = ⟨1, 0⟩)
29	22, 28	preq12d 4702	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} = {⟨0, 0⟩, ⟨1, 0⟩})
30	29	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
31	24	opeq2d 4850	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨1, ((𝑥 + 1) mod 𝑁)⟩ = ⟨1, ((0 + 1) mod 𝑁)⟩)
32	28, 31	preq12d 4702	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})
33	32	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩}))
34	27, 30, 33	3orbi123d 1463	. . . . . . . . 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 𝑁)⟩})))
35		eluzelre 12989	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℝ)
36		1mod 14056	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 1 < 𝑁) → (1 mod 𝑁) = 1)
37	35, 16, 36	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (1 mod 𝑁) = 1)
38		1e0p1 12874	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
39	38	oveq1i 7440	. . . . . . . . . . . . 13 ⊢ (1 mod 𝑁) = ((0 + 1) mod 𝑁)
40	37, 39	eqtr3di 2813	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 = ((0 + 1) mod 𝑁))
41	40	opeq2d 4850	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨0, 1⟩ = ⟨0, ((0 + 1) mod 𝑁)⟩)
42	41	preq2d 4701	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩})
43	42	3mix1d 1355	. . . . . . . . 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 𝑁)⟩}))
44	34, 10, 43	rspcedvdw 3583	. . . . . . . 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 𝑁)⟩}))
45	21, 44	jca 521	. . . . . . 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 𝑁)⟩})))
46		fveq2 6896	. . . . . . . . . 10 ⊢ (𝑋 = 0 → (𝐹‘𝑋) = (𝐹‘0))
47		gpgprismgr4cycllem1.f	. . . . . . . . . . . 12 ⊢ 𝐹 = ⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩
48	47	fveq1i 6897	. . . . . . . . . . 11 ⊢ (𝐹‘0) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘0)
49		prex 5400	. . . . . . . . . . . 12 ⊢ {⟨0, 0⟩, ⟨0, 1⟩} ∈ V
50		s4fv0 15061	. . . . . . . . . . . 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⟩})
51	49, 50	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⟩}
52	48, 51	eqtri 2786	. . . . . . . . . 10 ⊢ (𝐹‘0) = {⟨0, 0⟩, ⟨0, 1⟩}
53	46, 52	eqtrdi 2814	. . . . . . . . 9 ⊢ (𝑋 = 0 → (𝐹‘𝑋) = {⟨0, 0⟩, ⟨0, 1⟩})
54	53	eleq1d 2849	. . . . . . . 8 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
55	53	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
56	53	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
57	53	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
58	55, 56, 57	3orbi123d 1463	. . . . . . . . 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 𝑁)⟩})))
59	58	rexbidv 3190	. . . . . . . 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 𝑁)⟩})))
60	54, 59	anbi12d 644	. . . . . . 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 𝑁)⟩}))))
61	45, 60	imbitrrid 249	. . . . . 6 ⊢ (𝑋 = 0 → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
62		1elpr01 11317	. . . . . . . . . . 11 ⊢ 1 ∈ {0, 1}
63	62	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ {0, 1})
64	63, 18	opelxpd 5694	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁)))
65		prelpwi 5419	. . . . . . . . 9 ⊢ ((⟨0, 1⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
66	19, 64, 65	syl2anc 596	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
67		opeq2 4844	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨0, 𝑥⟩ = ⟨0, 1⟩)
68		oveq1 7437	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (𝑥 + 1) = (1 + 1))
69	68	oveq1d 7445	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → ((𝑥 + 1) mod 𝑁) = ((1 + 1) mod 𝑁))
70	69	opeq2d 4850	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨0, ((𝑥 + 1) mod 𝑁)⟩ = ⟨0, ((1 + 1) mod 𝑁)⟩)
71	67, 70	preq12d 4702	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} = {⟨0, 1⟩, ⟨0, ((1 + 1) mod 𝑁)⟩})
72	71	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨0, ((1 + 1) mod 𝑁)⟩}))
73		opeq2 4844	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨1, 𝑥⟩ = ⟨1, 1⟩)
74	67, 73	preq12d 4702	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} = {⟨0, 1⟩, ⟨1, 1⟩})
75	74	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨1, 1⟩}))
76	69	opeq2d 4850	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨1, ((𝑥 + 1) mod 𝑁)⟩ = ⟨1, ((1 + 1) mod 𝑁)⟩)
77	73, 76	preq12d 4702	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} = {⟨1, 1⟩, ⟨1, ((1 + 1) mod 𝑁)⟩})
78	77	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 1⟩, ⟨1, ((1 + 1) mod 𝑁)⟩}))
79	72, 75, 78	3orbi123d 1463	. . . . . . . . 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 𝑁)⟩})))
80		eqid 2763	. . . . . . . . . . 11 ⊢ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨1, 1⟩}
81	80	3mix2i 1353	. . . . . . . . . 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 𝑁)⟩})
82	81	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 𝑁)⟩}))
83	79, 18, 82	rspcedvdw 3583	. . . . . . . 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 𝑁)⟩}))
84	66, 83	jca 521	. . . . . . 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 𝑁)⟩})))
85		fveq2 6896	. . . . . . . . . 10 ⊢ (𝑋 = 1 → (𝐹‘𝑋) = (𝐹‘1))
86	47	fveq1i 6897	. . . . . . . . . . 11 ⊢ (𝐹‘1) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘1)
87		prex 5400	. . . . . . . . . . . 12 ⊢ {⟨0, 1⟩, ⟨1, 1⟩} ∈ V
88		s4fv1 15062	. . . . . . . . . . . 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⟩})
89	87, 88	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⟩}
90	86, 89	eqtri 2786	. . . . . . . . . 10 ⊢ (𝐹‘1) = {⟨0, 1⟩, ⟨1, 1⟩}
91	85, 90	eqtrdi 2814	. . . . . . . . 9 ⊢ (𝑋 = 1 → (𝐹‘𝑋) = {⟨0, 1⟩, ⟨1, 1⟩})
92	91	eleq1d 2849	. . . . . . . 8 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
93	91	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
94	91	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
95	91	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
96	93, 94, 95	3orbi123d 1463	. . . . . . . . 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 𝑁)⟩})))
97	96	rexbidv 3190	. . . . . . . 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 𝑁)⟩})))
98	92, 97	anbi12d 644	. . . . . . 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 𝑁)⟩}))))
99	84, 98	imbitrrid 249	. . . . . 6 ⊢ (𝑋 = 1 → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
100	61, 99	jaoi 871	. . . . 5 ⊢ ((𝑋 = 0 ∨ 𝑋 = 1) → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
101	5, 100	syl 18	. . . 4 ⊢ (𝑋 ∈ {0, 1} → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
102		elpri 4608	. . . . 5 ⊢ (𝑋 ∈ {2, 3} → (𝑋 = 2 ∨ 𝑋 = 3))
103	63, 10	opelxpd 5694	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁)))
104	64, 103	jca 521	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁))))
105	104	adantr 486	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 = 2) → (⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁))))
106		prelpwi 5419	. . . . . . . . . 10 ⊢ ((⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨1, 1⟩, ⟨1, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
107	105, 106	syl 18	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 = 2) → {⟨1, 1⟩, ⟨1, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
108	26	eqeq2d 2774	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
109	29	eqeq2d 2774	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
110	32	eqeq2d 2774	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩}))
111	108, 109, 110	3orbi123d 1463	. . . . . . . . . . 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 𝑁)⟩})))
112		prcom 4693	. . . . . . . . . . . . 13 ⊢ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 0⟩, ⟨1, 1⟩}
113	40	opeq2d 4850	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨1, 1⟩ = ⟨1, ((0 + 1) mod 𝑁)⟩)
114	113	preq2d 4701	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨1, 0⟩, ⟨1, 1⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})
115	112, 114	eqtrid 2810	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})
116	115	3mix3d 1357	. . . . . . . . . . 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 𝑁)⟩}))
117	111, 10, 116	rspcedvdw 3583	. . . . . . . . . 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 𝑁)⟩}))
118	117	adantr 486	. . . . . . . . 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 𝑁)⟩}))
119	107, 118	jca 521	. . . . . . . 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 𝑁)⟩})))
120		fveq2 6896	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → (𝐹‘𝑋) = (𝐹‘2))
121	47	fveq1i 6897	. . . . . . . . . . . . 13 ⊢ (𝐹‘2) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘2)
122		prex 5400	. . . . . . . . . . . . . 14 ⊢ {⟨1, 1⟩, ⟨1, 0⟩} ∈ V
123		s4fv2 15063	. . . . . . . . . . . . . 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⟩})
124	122, 123	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⟩}
125	121, 124	eqtri 2786	. . . . . . . . . . . 12 ⊢ (𝐹‘2) = {⟨1, 1⟩, ⟨1, 0⟩}
126	120, 125	eqtrdi 2814	. . . . . . . . . . 11 ⊢ (𝑋 = 2 → (𝐹‘𝑋) = {⟨1, 1⟩, ⟨1, 0⟩})
127	126	eleq1d 2849	. . . . . . . . . 10 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨1, 1⟩, ⟨1, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
128	126	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
129	126	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
130	126	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
131	128, 129, 130	3orbi123d 1463	. . . . . . . . . . 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 𝑁)⟩})))
132	131	rexbidv 3190	. . . . . . . . . 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 𝑁)⟩})))
133	127, 132	anbi12d 644	. . . . . . . . 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 𝑁)⟩}))))
134	133	adantl 487	. . . . . . . 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 𝑁)⟩}))))
135	119, 134	mpbird 260	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 = 2) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
136	135	expcom 419	. . . . . 6 ⊢ (𝑋 = 2 → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
137		prelpwi 5419	. . . . . . . . 9 ⊢ ((⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨0, 0⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
138	103, 11, 137	syl2anc 596	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
139	26	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
140	29	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
141	32	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩}))
142	139, 140, 141	3orbi123d 1463	. . . . . . . . 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 𝑁)⟩})))
143		prcom 4693	. . . . . . . . . . 11 ⊢ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩}
144	143	3mix2i 1353	. . . . . . . . . 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 𝑁)⟩})
145	144	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 𝑁)⟩}))
146	142, 10, 145	rspcedvdw 3583	. . . . . . . 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 𝑁)⟩}))
147	138, 146	jca 521	. . . . . . 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 𝑁)⟩})))
148		fveq2 6896	. . . . . . . . . 10 ⊢ (𝑋 = 3 → (𝐹‘𝑋) = (𝐹‘3))
149	47	fveq1i 6897	. . . . . . . . . . 11 ⊢ (𝐹‘3) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘3)
150		prex 5400	. . . . . . . . . . . 12 ⊢ {⟨1, 0⟩, ⟨0, 0⟩} ∈ V
151		s4fv3 15064	. . . . . . . . . . . 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⟩})
152	150, 151	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⟩}
153	149, 152	eqtri 2786	. . . . . . . . . 10 ⊢ (𝐹‘3) = {⟨1, 0⟩, ⟨0, 0⟩}
154	148, 153	eqtrdi 2814	. . . . . . . . 9 ⊢ (𝑋 = 3 → (𝐹‘𝑋) = {⟨1, 0⟩, ⟨0, 0⟩})
155	154	eleq1d 2849	. . . . . . . 8 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
156	154	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
157	154	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
158	154	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
159	156, 157, 158	3orbi123d 1463	. . . . . . . . 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 𝑁)⟩})))
160	159	rexbidv 3190	. . . . . . . 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 𝑁)⟩})))
161	155, 160	anbi12d 644	. . . . . . 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 𝑁)⟩}))))
162	147, 161	imbitrrid 249	. . . . . 6 ⊢ (𝑋 = 3 → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
163	136, 162	jaoi 871	. . . . 5 ⊢ ((𝑋 = 2 ∨ 𝑋 = 3) → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
164	102, 163	syl 18	. . . 4 ⊢ (𝑋 ∈ {2, 3} → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
165	101, 164	jaoi 871	. . 3 ⊢ ((𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}) → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
166	4, 165	sylbi 220	. 2 ⊢ (𝑋 ∈ (0..^4) → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
167	166	impcom 413	1 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 ∈ (0..^4)) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∨ w3o 1102 = wceq 1569 ∈ wcel 2146 ∃wrex 3090 Vcvv 3454 ∪ cun 4152 𝒫 cpw 4560 {cpr 4590 ⟨cop 4838 class class class wbr 5106 × cxp 5653 ‘cfv 6547 (class class class)co 7430 ℝcr 11212 0cc0 11213 1c1 11214 + caddc 11216 < clt 11356 ℕcn 12348 2c2 12410 3c3 12411 4c4 12412 ℕ₀cn0 12619 ℤ_≥cuz 12978 ..^cfzo 13801 mod cmo 14022 ⟨“cs4 15008

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7761 ax-cnex 11269 ax-resscn 11270 ax-1cn 11271 ax-icn 11272 ax-addcl 11273 ax-addrcl 11274 ax-mulcl 11275 ax-mulrcl 11276 ax-mulcom 11277 ax-addass 11278 ax-mulass 11279 ax-distr 11280 ax-i2m1 11281 ax-1ne0 11282 ax-1rid 11283 ax-rnegex 11284 ax-rrecex 11285 ax-cnre 11286 ax-pre-lttri 11287 ax-pre-lttrn 11288 ax-pre-ltadd 11289 ax-pre-mulgt0 11290 ax-pre-sup 11291

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6311 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6501 df-fun 6549 df-fn 6550 df-f 6551 df-f1 6552 df-fo 6553 df-f1o 6554 df-fv 6555 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-om 7888 df-1st 8011 df-2nd 8012 df-frecs 8313 df-wrecs 8344 df-recs 8393 df-rdg 8432 df-1o 8490 df-er 8731 df-en 8988 df-dom 8989 df-sdom 8990 df-fin 8991 df-sup 9447 df-inf 9448 df-card 10033 df-pnf 11358 df-mnf 11359 df-xr 11360 df-ltxr 11361 df-le 11362 df-sub 11556 df-neg 11557 df-div 11987 df-nn 12349 df-2 12418 df-3 12419 df-4 12420 df-n0 12620 df-z 12707 df-uz 12979 df-rp 13134 df-fz 13653 df-fzo 13802 df-fl 13945 df-mod 14023 df-hash 14488 df-word 14672 df-concat 14729 df-s1 14756 df-s2 15013 df-s3 15014 df-s4 15015

This theorem is used by: gpgprismgr4cycllem10 49347

W3C validator