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 48785

Description: Lemma 3 for gpgprismgr4cycl0 48794. (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 13782	. . . . 5 ⊢ (0..^4) = ({0, 1} ∪ {2, 3})
2	1	eleq2i 2861	. . . 4 ⊢ (𝑋 ∈ (0..^4) ↔ 𝑋 ∈ ({0, 1} ∪ {2, 3}))
3		elun 4115	. . . 4 ⊢ (𝑋 ∈ ({0, 1} ∪ {2, 3}) ↔ (𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}))
4	2, 3	bitri 278	. . 3 ⊢ (𝑋 ∈ (0..^4) ↔ (𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}))
5		elpri 4618	. . . . 5 ⊢ (𝑋 ∈ {0, 1} → (𝑋 = 0 ∨ 𝑋 = 1))
6		c0ex 11200	. . . . . . . . . . . 12 ⊢ 0 ∈ V
7	6	prid1 4733	. . . . . . . . . . 11 ⊢ 0 ∈ {0, 1}
8	7	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 0 ∈ {0, 1})
9		eluz3nn 12913	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℕ)
10		lbfzo0 13728	. . . . . . . . . . 11 ⊢ (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
11	9, 10	sylibr 237	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 0 ∈ (0..^𝑁))
12	8, 11	opelxpd 5701	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨0, 0⟩ ∈ ({0, 1} × (0..^𝑁)))
13		1nn0 12520	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ₀
14	13	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ ℕ₀)
15		uzuzle23 12908	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ (ℤ_≥‘2))
16		eluz2gt1 12944	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 1 < 𝑁)
17	15, 16	syl 18	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 < 𝑁)
18		elfzo0 13729	. . . . . . . . . . 11 ⊢ (1 ∈ (0..^𝑁) ↔ (1 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 1 < 𝑁))
19	14, 9, 17, 18	syl3anbrc 1360	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ (0..^𝑁))
20	8, 19	opelxpd 5701	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨0, 1⟩ ∈ ({0, 1} × (0..^𝑁)))
21		prelpwi 5429	. . . . . . . . 9 ⊢ ((⟨0, 0⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨0, 1⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
22	12, 20, 21	syl2anc 595	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
23		opeq2 4843	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨0, 𝑥⟩ = ⟨0, 0⟩)
24		oveq1 7418	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1))
25	24	oveq1d 7426	. . . . . . . . . . . . 13 ⊢ (𝑥 = 0 → ((𝑥 + 1) mod 𝑁) = ((0 + 1) mod 𝑁))
26	25	opeq2d 4849	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨0, ((𝑥 + 1) mod 𝑁)⟩ = ⟨0, ((0 + 1) mod 𝑁)⟩)
27	23, 26	preq12d 4712	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩})
28	27	eqeq2d 2780	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
29		opeq2 4843	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨1, 𝑥⟩ = ⟨1, 0⟩)
30	23, 29	preq12d 4712	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} = {⟨0, 0⟩, ⟨1, 0⟩})
31	30	eqeq2d 2780	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
32	25	opeq2d 4849	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨1, ((𝑥 + 1) mod 𝑁)⟩ = ⟨1, ((0 + 1) mod 𝑁)⟩)
33	29, 32	preq12d 4712	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})
34	33	eqeq2d 2780	. . . . . . . . . 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 1461	. . . . . . . . 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 12873	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℝ)
37		1mod 13936	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 1 < 𝑁) → (1 mod 𝑁) = 1)
38	36, 17, 37	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (1 mod 𝑁) = 1)
39		1e0p1 12758	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
40	39	oveq1i 7421	. . . . . . . . . . . . 13 ⊢ (1 mod 𝑁) = ((0 + 1) mod 𝑁)
41	38, 40	eqtr3di 2819	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 = ((0 + 1) mod 𝑁))
42	41	opeq2d 4849	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨0, 1⟩ = ⟨0, ((0 + 1) mod 𝑁)⟩)
43	42	preq2d 4711	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩})
44	43	3mix1d 1353	. . . . . . . . 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 3593	. . . . . . . 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 520	. . . . . . 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 6882	. . . . . . . . . 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 6883	. . . . . . . . . . 11 ⊢ (𝐹‘0) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘0)
50		prex 5410	. . . . . . . . . . . 12 ⊢ {⟨0, 0⟩, ⟨0, 1⟩} ∈ V
51		s4fv0 14932	. . . . . . . . . . . 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 2792	. . . . . . . . . 10 ⊢ (𝐹‘0) = {⟨0, 0⟩, ⟨0, 1⟩}
54	47, 53	eqtrdi 2820	. . . . . . . . 9 ⊢ (𝑋 = 0 → (𝐹‘𝑋) = {⟨0, 0⟩, ⟨0, 1⟩})
55	54	eleq1d 2854	. . . . . . . 8 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
56	54	eqeq1d 2771	. . . . . . . . . 10 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
57	54	eqeq1d 2771	. . . . . . . . . 10 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
58	54	eqeq1d 2771	. . . . . . . . . 10 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
59	56, 57, 58	3orbi123d 1461	. . . . . . . . 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 3195	. . . . . . . 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 643	. . . . . . 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 249	. . . . . 6 ⊢ (𝑋 = 0 → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
63		1ex 11203	. . . . . . . . . . . 12 ⊢ 1 ∈ V
64	63	prid2 4734	. . . . . . . . . . 11 ⊢ 1 ∈ {0, 1}
65	64	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ {0, 1})
66	65, 19	opelxpd 5701	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁)))
67		prelpwi 5429	. . . . . . . . 9 ⊢ ((⟨0, 1⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
68	20, 66, 67	syl2anc 595	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
69		opeq2 4843	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨0, 𝑥⟩ = ⟨0, 1⟩)
70		oveq1 7418	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (𝑥 + 1) = (1 + 1))
71	70	oveq1d 7426	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → ((𝑥 + 1) mod 𝑁) = ((1 + 1) mod 𝑁))
72	71	opeq2d 4849	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨0, ((𝑥 + 1) mod 𝑁)⟩ = ⟨0, ((1 + 1) mod 𝑁)⟩)
73	69, 72	preq12d 4712	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} = {⟨0, 1⟩, ⟨0, ((1 + 1) mod 𝑁)⟩})
74	73	eqeq2d 2780	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨0, ((1 + 1) mod 𝑁)⟩}))
75		opeq2 4843	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨1, 𝑥⟩ = ⟨1, 1⟩)
76	69, 75	preq12d 4712	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} = {⟨0, 1⟩, ⟨1, 1⟩})
77	76	eqeq2d 2780	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨1, 1⟩}))
78	71	opeq2d 4849	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨1, ((𝑥 + 1) mod 𝑁)⟩ = ⟨1, ((1 + 1) mod 𝑁)⟩)
79	75, 78	preq12d 4712	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} = {⟨1, 1⟩, ⟨1, ((1 + 1) mod 𝑁)⟩})
80	79	eqeq2d 2780	. . . . . . . . . 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 1461	. . . . . . . . 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 2769	. . . . . . . . . . 11 ⊢ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨1, 1⟩}
83	82	3mix2i 1351	. . . . . . . . . 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 3593	. . . . . . . 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 520	. . . . . . 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 6882	. . . . . . . . . 10 ⊢ (𝑋 = 1 → (𝐹‘𝑋) = (𝐹‘1))
88	48	fveq1i 6883	. . . . . . . . . . 11 ⊢ (𝐹‘1) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘1)
89		prex 5410	. . . . . . . . . . . 12 ⊢ {⟨0, 1⟩, ⟨1, 1⟩} ∈ V
90		s4fv1 14933	. . . . . . . . . . . 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 2792	. . . . . . . . . 10 ⊢ (𝐹‘1) = {⟨0, 1⟩, ⟨1, 1⟩}
93	87, 92	eqtrdi 2820	. . . . . . . . 9 ⊢ (𝑋 = 1 → (𝐹‘𝑋) = {⟨0, 1⟩, ⟨1, 1⟩})
94	93	eleq1d 2854	. . . . . . . 8 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
95	93	eqeq1d 2771	. . . . . . . . . 10 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
96	93	eqeq1d 2771	. . . . . . . . . 10 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
97	93	eqeq1d 2771	. . . . . . . . . 10 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
98	95, 96, 97	3orbi123d 1461	. . . . . . . . 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 3195	. . . . . . . 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 643	. . . . . . 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 249	. . . . . 6 ⊢ (𝑋 = 1 → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
102	62, 101	jaoi 870	. . . . 5 ⊢ ((𝑋 = 0 ∨ 𝑋 = 1) → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
103	5, 102	syl 18	. . . 4 ⊢ (𝑋 ∈ {0, 1} → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
104		elpri 4618	. . . . 5 ⊢ (𝑋 ∈ {2, 3} → (𝑋 = 2 ∨ 𝑋 = 3))
105	65, 11	opelxpd 5701	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁)))
106	66, 105	jca 520	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁))))
107	106	adantr 485	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 = 2) → (⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁))))
108		prelpwi 5429	. . . . . . . . . 10 ⊢ ((⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨1, 1⟩, ⟨1, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
109	107, 108	syl 18	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 = 2) → {⟨1, 1⟩, ⟨1, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
110	27	eqeq2d 2780	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
111	30	eqeq2d 2780	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
112	33	eqeq2d 2780	. . . . . . . . . . . 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 1461	. . . . . . . . . . 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 4703	. . . . . . . . . . . . 13 ⊢ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 0⟩, ⟨1, 1⟩}
115	41	opeq2d 4849	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨1, 1⟩ = ⟨1, ((0 + 1) mod 𝑁)⟩)
116	115	preq2d 4711	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨1, 0⟩, ⟨1, 1⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})
117	114, 116	eqtrid 2816	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})
118	117	3mix3d 1355	. . . . . . . . . . 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 3593	. . . . . . . . . 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 485	. . . . . . . . 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 520	. . . . . . . 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 6882	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → (𝐹‘𝑋) = (𝐹‘2))
123	48	fveq1i 6883	. . . . . . . . . . . . 13 ⊢ (𝐹‘2) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘2)
124		prex 5410	. . . . . . . . . . . . . 14 ⊢ {⟨1, 1⟩, ⟨1, 0⟩} ∈ V
125		s4fv2 14934	. . . . . . . . . . . . . 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 2792	. . . . . . . . . . . 12 ⊢ (𝐹‘2) = {⟨1, 1⟩, ⟨1, 0⟩}
128	122, 127	eqtrdi 2820	. . . . . . . . . . 11 ⊢ (𝑋 = 2 → (𝐹‘𝑋) = {⟨1, 1⟩, ⟨1, 0⟩})
129	128	eleq1d 2854	. . . . . . . . . 10 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨1, 1⟩, ⟨1, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
130	128	eqeq1d 2771	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
131	128	eqeq1d 2771	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
132	128	eqeq1d 2771	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
133	130, 131, 132	3orbi123d 1461	. . . . . . . . . . 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 3195	. . . . . . . . . 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 643	. . . . . . . . 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 486	. . . . . . . 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 260	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑋 = 2) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
138	137	expcom 418	. . . . . 6 ⊢ (𝑋 = 2 → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
139		prelpwi 5429	. . . . . . . . 9 ⊢ ((⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨0, 0⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
140	105, 12, 139	syl2anc 595	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
141	27	eqeq2d 2780	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
142	30	eqeq2d 2780	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
143	33	eqeq2d 2780	. . . . . . . . . 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 1461	. . . . . . . . 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 4703	. . . . . . . . . . 11 ⊢ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩}
146	145	3mix2i 1351	. . . . . . . . . 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 3593	. . . . . . . 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 520	. . . . . . 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 6882	. . . . . . . . . 10 ⊢ (𝑋 = 3 → (𝐹‘𝑋) = (𝐹‘3))
151	48	fveq1i 6883	. . . . . . . . . . 11 ⊢ (𝐹‘3) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘3)
152		prex 5410	. . . . . . . . . . . 12 ⊢ {⟨1, 0⟩, ⟨0, 0⟩} ∈ V
153		s4fv3 14935	. . . . . . . . . . . 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 2792	. . . . . . . . . 10 ⊢ (𝐹‘3) = {⟨1, 0⟩, ⟨0, 0⟩}
156	150, 155	eqtrdi 2820	. . . . . . . . 9 ⊢ (𝑋 = 3 → (𝐹‘𝑋) = {⟨1, 0⟩, ⟨0, 0⟩})
157	156	eleq1d 2854	. . . . . . . 8 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
158	156	eqeq1d 2771	. . . . . . . . . 10 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
159	156	eqeq1d 2771	. . . . . . . . . 10 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
160	156	eqeq1d 2771	. . . . . . . . . 10 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
161	158, 159, 160	3orbi123d 1461	. . . . . . . . 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 3195	. . . . . . . 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 643	. . . . . . 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 249	. . . . . 6 ⊢ (𝑋 = 3 → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
165	138, 164	jaoi 870	. . . . 5 ⊢ ((𝑋 = 2 ∨ 𝑋 = 3) → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
166	104, 165	syl 18	. . . 4 ⊢ (𝑋 ∈ {2, 3} → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
167	103, 166	jaoi 870	. . 3 ⊢ ((𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}) → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
168	4, 167	sylbi 220	. 2 ⊢ (𝑋 ∈ (0..^4) → (𝑁 ∈ (ℤ_≥‘3) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))))
169	168	impcom 412	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 209 ∧ wa 400 ∨ wo 860 ∨ w3o 1100 = wceq 1567 ∈ wcel 2149 ∃wrex 3095 Vcvv 3463 ∪ cun 3911 𝒫 cpw 4567 {cpr 4596 ⟨cop 4600 class class class wbr 5113 × cxp 5660 ‘cfv 6537 (class class class)co 7411 ℝcr 11099 0cc0 11100 1c1 11101 + caddc 11103 < clt 11243 ℕcn 12233 2c2 12295 3c3 12296 4c4 12297 ℕ₀cn0 12504 ℤ_≥cuz 12862 ..^cfzo 13682 mod cmo 13902 ⟨“cs4 14880

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-pre-sup 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-er 8694 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-sup 9402 df-inf 9403 df-card 9925 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-div 11872 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-n0 12505 df-z 12592 df-uz 12863 df-rp 13017 df-fz 13536 df-fzo 13683 df-fl 13825 df-mod 13903 df-hash 14367 df-word 14551 df-concat 14608 df-s1 14634 df-s2 14885 df-s3 14886 df-s4 14887

This theorem is referenced by: gpgprismgr4cycllem10 48792

W3C validator