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 49027

Description: Lemma 3 for gpgprismgr4cycl0 49036. (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 13831	. . . . 5 ⊢ (0..^4) = ({0, 1} ∪ {2, 3})
2	1	eleq2i 2852	. . . 4 ⊢ (𝑋 ∈ (0..^4) ↔ 𝑋 ∈ ({0, 1} ∪ {2, 3}))
3		elun 4100	. . . 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 11247	. . . . . . . . . . 11 ⊢ 0 ∈ {0, 1}
7	6	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 0 ∈ {0, 1})
8		eluz3nn 12960	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℕ)
9		lbfzo0 13777	. . . . . . . . . . 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 12566	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ₀
13	12	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ ℕ₀)
14		uzuzle23 12955	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ (ℤ_≥‘2))
15		eluz2gt1 12991	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 1 < 𝑁)
16	14, 15	syl 18	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 < 𝑁)
17		elfzo0 13778	. . . . . . . . . . 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 5422	. . . . . . . . 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 4834	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨0, 𝑥⟩ = ⟨0, 0⟩)
23		oveq1 7422	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1))
24	23	oveq1d 7430	. . . . . . . . . . . . 13 ⊢ (𝑥 = 0 → ((𝑥 + 1) mod 𝑁) = ((0 + 1) mod 𝑁))
25	24	opeq2d 4840	. . . . . . . . . . . 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 2771	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
28		opeq2 4834	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨1, 𝑥⟩ = ⟨1, 0⟩)
29	22, 28	preq12d 4702	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} = {⟨0, 0⟩, ⟨1, 0⟩})
30	29	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
31	24	opeq2d 4840	. . . . . . . . . . . 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 2771	. . . . . . . . . 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 12920	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℝ)
36		1mod 13986	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 1 < 𝑁) → (1 mod 𝑁) = 1)
37	35, 16, 36	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (1 mod 𝑁) = 1)
38		1e0p1 12805	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
39	38	oveq1i 7425	. . . . . . . . . . . . 13 ⊢ (1 mod 𝑁) = ((0 + 1) mod 𝑁)
40	37, 39	eqtr3di 2810	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 = ((0 + 1) mod 𝑁))
41	40	opeq2d 4840	. . . . . . . . . . 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 3579	. . . . . . . 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 6880	. . . . . . . . . 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 6881	. . . . . . . . . . 11 ⊢ (𝐹‘0) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘0)
49		prex 5403	. . . . . . . . . . . 12 ⊢ {⟨0, 0⟩, ⟨0, 1⟩} ∈ V
50		s4fv0 14988	. . . . . . . . . . . 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 2783	. . . . . . . . . 10 ⊢ (𝐹‘0) = {⟨0, 0⟩, ⟨0, 1⟩}
53	46, 52	eqtrdi 2811	. . . . . . . . 9 ⊢ (𝑋 = 0 → (𝐹‘𝑋) = {⟨0, 0⟩, ⟨0, 1⟩})
54	53	eleq1d 2845	. . . . . . . 8 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
55	53	eqeq1d 2762	. . . . . . . . . 10 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
56	53	eqeq1d 2762	. . . . . . . . . 10 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
57	53	eqeq1d 2762	. . . . . . . . . 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 3186	. . . . . . . 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 11250	. . . . . . . . . . 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 5422	. . . . . . . . 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 4834	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨0, 𝑥⟩ = ⟨0, 1⟩)
68		oveq1 7422	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (𝑥 + 1) = (1 + 1))
69	68	oveq1d 7430	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → ((𝑥 + 1) mod 𝑁) = ((1 + 1) mod 𝑁))
70	69	opeq2d 4840	. . . . . . . . . . . 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 2771	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨0, ((1 + 1) mod 𝑁)⟩}))
73		opeq2 4834	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨1, 𝑥⟩ = ⟨1, 1⟩)
74	67, 73	preq12d 4702	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} = {⟨0, 1⟩, ⟨1, 1⟩})
75	74	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨1, 1⟩}))
76	69	opeq2d 4840	. . . . . . . . . . . 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 2771	. . . . . . . . . 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 2760	. . . . . . . . . . 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 3579	. . . . . . . 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 6880	. . . . . . . . . 10 ⊢ (𝑋 = 1 → (𝐹‘𝑋) = (𝐹‘1))
86	47	fveq1i 6881	. . . . . . . . . . 11 ⊢ (𝐹‘1) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘1)
87		prex 5403	. . . . . . . . . . . 12 ⊢ {⟨0, 1⟩, ⟨1, 1⟩} ∈ V
88		s4fv1 14989	. . . . . . . . . . . 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 2783	. . . . . . . . . 10 ⊢ (𝐹‘1) = {⟨0, 1⟩, ⟨1, 1⟩}
91	85, 90	eqtrdi 2811	. . . . . . . . 9 ⊢ (𝑋 = 1 → (𝐹‘𝑋) = {⟨0, 1⟩, ⟨1, 1⟩})
92	91	eleq1d 2845	. . . . . . . 8 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
93	91	eqeq1d 2762	. . . . . . . . . 10 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
94	91	eqeq1d 2762	. . . . . . . . . 10 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
95	91	eqeq1d 2762	. . . . . . . . . 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 3186	. . . . . . . 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 5422	. . . . . . . . . 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 2771	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
109	29	eqeq2d 2771	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
110	32	eqeq2d 2771	. . . . . . . . . . . 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 4840	. . . . . . . . . . . . . 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 2807	. . . . . . . . . . . 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 3579	. . . . . . . . . 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 6880	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → (𝐹‘𝑋) = (𝐹‘2))
121	47	fveq1i 6881	. . . . . . . . . . . . 13 ⊢ (𝐹‘2) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘2)
122		prex 5403	. . . . . . . . . . . . . 14 ⊢ {⟨1, 1⟩, ⟨1, 0⟩} ∈ V
123		s4fv2 14990	. . . . . . . . . . . . . 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 2783	. . . . . . . . . . . 12 ⊢ (𝐹‘2) = {⟨1, 1⟩, ⟨1, 0⟩}
126	120, 125	eqtrdi 2811	. . . . . . . . . . 11 ⊢ (𝑋 = 2 → (𝐹‘𝑋) = {⟨1, 1⟩, ⟨1, 0⟩})
127	126	eleq1d 2845	. . . . . . . . . 10 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨1, 1⟩, ⟨1, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
128	126	eqeq1d 2762	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
129	126	eqeq1d 2762	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
130	126	eqeq1d 2762	. . . . . . . . . . . 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 3186	. . . . . . . . . 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 5422	. . . . . . . . 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 2771	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
140	29	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
141	32	eqeq2d 2771	. . . . . . . . . 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 3579	. . . . . . . 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 6880	. . . . . . . . . 10 ⊢ (𝑋 = 3 → (𝐹‘𝑋) = (𝐹‘3))
149	47	fveq1i 6881	. . . . . . . . . . 11 ⊢ (𝐹‘3) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘3)
150		prex 5403	. . . . . . . . . . . 12 ⊢ {⟨1, 0⟩, ⟨0, 0⟩} ∈ V
151		s4fv3 14991	. . . . . . . . . . . 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 2783	. . . . . . . . . 10 ⊢ (𝐹‘3) = {⟨1, 0⟩, ⟨0, 0⟩}
154	148, 153	eqtrdi 2811	. . . . . . . . 9 ⊢ (𝑋 = 3 → (𝐹‘𝑋) = {⟨1, 0⟩, ⟨0, 0⟩})
155	154	eleq1d 2845	. . . . . . . 8 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
156	154	eqeq1d 2762	. . . . . . . . . 10 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
157	154	eqeq1d 2762	. . . . . . . . . 10 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
158	154	eqeq1d 2762	. . . . . . . . . 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 3186	. . . . . . . 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 1570 ∈ wcel 2145 ∃wrex 3086 Vcvv 3450 ∪ cun 3897 𝒫 cpw 4557 {cpr 4586 ⟨cop 4590 class class class wbr 5103 × cxp 5653 ‘cfv 6534 (class class class)co 7415 ℝcr 11145 0cc0 11146 1c1 11147 + caddc 11149 < clt 11289 ℕcn 12279 2c2 12341 3c3 12342 4c4 12343 ℕ₀cn0 12550 ℤ_≥cuz 12909 ..^cfzo 13731 mod cmo 13952 ⟨“cs4 14936

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7738 ax-cnex 11202 ax-resscn 11203 ax-1cn 11204 ax-icn 11205 ax-addcl 11206 ax-addrcl 11207 ax-mulcl 11208 ax-mulrcl 11209 ax-mulcom 11210 ax-addass 11211 ax-mulass 11212 ax-distr 11213 ax-i2m1 11214 ax-1ne0 11215 ax-1rid 11216 ax-rnegex 11217 ax-rrecex 11218 ax-cnre 11219 ax-pre-lttri 11220 ax-pre-lttrn 11221 ax-pre-ltadd 11222 ax-pre-mulgt0 11223 ax-pre-sup 11224

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 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 6300 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6490 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-riota 7372 df-ov 7418 df-oprab 7419 df-mpo 7420 df-om 7865 df-1st 7988 df-2nd 7989 df-frecs 8282 df-wrecs 8313 df-recs 8362 df-rdg 8401 df-1o 8459 df-er 8700 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-sup 9416 df-inf 9417 df-card 9966 df-pnf 11291 df-mnf 11292 df-xr 11293 df-ltxr 11294 df-le 11295 df-sub 11489 df-neg 11490 df-div 11918 df-nn 12280 df-2 12349 df-3 12350 df-4 12351 df-n0 12551 df-z 12638 df-uz 12910 df-rp 13065 df-fz 13584 df-fzo 13732 df-fl 13875 df-mod 13953 df-hash 14417 df-word 14601 df-concat 14658 df-s1 14685 df-s2 14941 df-s3 14942 df-s4 14943

This theorem is used by: gpgprismgr4cycllem10 49034

W3C validator