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 48091

Description: Lemma 3 for gpgprismgr4cycl0 48100. (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 13656	. . . . 5 ⊢ (0..^4) = ({0, 1} ∪ {2, 3})
2	1	eleq2i 2820	. . . 4 ⊢ (𝑋 ∈ (0..^4) ↔ 𝑋 ∈ ({0, 1} ∪ {2, 3}))
3		elun 4104	. . . 4 ⊢ (𝑋 ∈ ({0, 1} ∪ {2, 3}) ↔ (𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}))
4	2, 3	bitri 275	. . 3 ⊢ (𝑋 ∈ (0..^4) ↔ (𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}))
5		elpri 4601	. . . . 5 ⊢ (𝑋 ∈ {0, 1} → (𝑋 = 0 ∨ 𝑋 = 1))
6		c0ex 11109	. . . . . . . . . . . 12 ⊢ 0 ∈ V
7	6	prid1 4714	. . . . . . . . . . 11 ⊢ 0 ∈ {0, 1}
8	7	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 0 ∈ {0, 1})
9		eluz3nn 12790	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℕ)
10		lbfzo0 13602	. . . . . . . . . . 11 ⊢ (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
11	9, 10	sylibr 234	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 0 ∈ (0..^𝑁))
12	8, 11	opelxpd 5658	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨0, 0⟩ ∈ ({0, 1} × (0..^𝑁)))
13		1nn0 12400	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ₀
14	13	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ ℕ₀)
15		uzuzle23 12785	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ (ℤ_≥‘2))
16		eluz2gt1 12821	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 1 < 𝑁)
17	15, 16	syl 17	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 < 𝑁)
18		elfzo0 13603	. . . . . . . . . . 11 ⊢ (1 ∈ (0..^𝑁) ↔ (1 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 1 < 𝑁))
19	14, 9, 17, 18	syl3anbrc 1344	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ (0..^𝑁))
20	8, 19	opelxpd 5658	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨0, 1⟩ ∈ ({0, 1} × (0..^𝑁)))
21		prelpwi 5390	. . . . . . . . 9 ⊢ ((⟨0, 0⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨0, 1⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
22	12, 20, 21	syl2anc 584	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
23		opeq2 4825	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨0, 𝑥⟩ = ⟨0, 0⟩)
24		oveq1 7356	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1))
25	24	oveq1d 7364	. . . . . . . . . . . . 13 ⊢ (𝑥 = 0 → ((𝑥 + 1) mod 𝑁) = ((0 + 1) mod 𝑁))
26	25	opeq2d 4831	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨0, ((𝑥 + 1) mod 𝑁)⟩ = ⟨0, ((0 + 1) mod 𝑁)⟩)
27	23, 26	preq12d 4693	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩})
28	27	eqeq2d 2740	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
29		opeq2 4825	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨1, 𝑥⟩ = ⟨1, 0⟩)
30	23, 29	preq12d 4693	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} = {⟨0, 0⟩, ⟨1, 0⟩})
31	30	eqeq2d 2740	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
32	25	opeq2d 4831	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ⟨1, ((𝑥 + 1) mod 𝑁)⟩ = ⟨1, ((0 + 1) mod 𝑁)⟩)
33	29, 32	preq12d 4693	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})
34	33	eqeq2d 2740	. . . . . . . . . 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 1437	. . . . . . . . 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 12746	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℝ)
37		1mod 13807	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 1 < 𝑁) → (1 mod 𝑁) = 1)
38	36, 17, 37	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (1 mod 𝑁) = 1)
39		1e0p1 12633	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
40	39	oveq1i 7359	. . . . . . . . . . . . 13 ⊢ (1 mod 𝑁) = ((0 + 1) mod 𝑁)
41	38, 40	eqtr3di 2779	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 = ((0 + 1) mod 𝑁))
42	41	opeq2d 4831	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨0, 1⟩ = ⟨0, ((0 + 1) mod 𝑁)⟩)
43	42	preq2d 4692	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩})
44	43	3mix1d 1337	. . . . . . . . 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 3580	. . . . . . . 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 6822	. . . . . . . . . 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 6823	. . . . . . . . . . 11 ⊢ (𝐹‘0) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘0)
50		prex 5376	. . . . . . . . . . . 12 ⊢ {⟨0, 0⟩, ⟨0, 1⟩} ∈ V
51		s4fv0 14802	. . . . . . . . . . . 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 2752	. . . . . . . . . 10 ⊢ (𝐹‘0) = {⟨0, 0⟩, ⟨0, 1⟩}
54	47, 53	eqtrdi 2780	. . . . . . . . 9 ⊢ (𝑋 = 0 → (𝐹‘𝑋) = {⟨0, 0⟩, ⟨0, 1⟩})
55	54	eleq1d 2813	. . . . . . . 8 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨0, 0⟩, ⟨0, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
56	54	eqeq1d 2731	. . . . . . . . . 10 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
57	54	eqeq1d 2731	. . . . . . . . . 10 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
58	54	eqeq1d 2731	. . . . . . . . . 10 ⊢ (𝑋 = 0 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 0⟩, ⟨0, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
59	56, 57, 58	3orbi123d 1437	. . . . . . . . 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 3153	. . . . . . . 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 632	. . . . . . 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 11111	. . . . . . . . . . . 12 ⊢ 1 ∈ V
64	63	prid2 4715	. . . . . . . . . . 11 ⊢ 1 ∈ {0, 1}
65	64	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ {0, 1})
66	65, 19	opelxpd 5658	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁)))
67		prelpwi 5390	. . . . . . . . 9 ⊢ ((⟨0, 1⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨1, 1⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
68	20, 66, 67	syl2anc 584	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
69		opeq2 4825	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨0, 𝑥⟩ = ⟨0, 1⟩)
70		oveq1 7356	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (𝑥 + 1) = (1 + 1))
71	70	oveq1d 7364	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → ((𝑥 + 1) mod 𝑁) = ((1 + 1) mod 𝑁))
72	71	opeq2d 4831	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨0, ((𝑥 + 1) mod 𝑁)⟩ = ⟨0, ((1 + 1) mod 𝑁)⟩)
73	69, 72	preq12d 4693	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} = {⟨0, 1⟩, ⟨0, ((1 + 1) mod 𝑁)⟩})
74	73	eqeq2d 2740	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨0, ((1 + 1) mod 𝑁)⟩}))
75		opeq2 4825	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨1, 𝑥⟩ = ⟨1, 1⟩)
76	69, 75	preq12d 4693	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} = {⟨0, 1⟩, ⟨1, 1⟩})
77	76	eqeq2d 2740	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ({⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨1, 1⟩}))
78	71	opeq2d 4831	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ⟨1, ((𝑥 + 1) mod 𝑁)⟩ = ⟨1, ((1 + 1) mod 𝑁)⟩)
79	75, 78	preq12d 4693	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} = {⟨1, 1⟩, ⟨1, ((1 + 1) mod 𝑁)⟩})
80	79	eqeq2d 2740	. . . . . . . . . 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 1437	. . . . . . . . 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 2729	. . . . . . . . . . 11 ⊢ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 1⟩, ⟨1, 1⟩}
83	82	3mix2i 1335	. . . . . . . . . 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 3580	. . . . . . . 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 6822	. . . . . . . . . 10 ⊢ (𝑋 = 1 → (𝐹‘𝑋) = (𝐹‘1))
88	48	fveq1i 6823	. . . . . . . . . . 11 ⊢ (𝐹‘1) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘1)
89		prex 5376	. . . . . . . . . . . 12 ⊢ {⟨0, 1⟩, ⟨1, 1⟩} ∈ V
90		s4fv1 14803	. . . . . . . . . . . 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 2752	. . . . . . . . . 10 ⊢ (𝐹‘1) = {⟨0, 1⟩, ⟨1, 1⟩}
93	87, 92	eqtrdi 2780	. . . . . . . . 9 ⊢ (𝑋 = 1 → (𝐹‘𝑋) = {⟨0, 1⟩, ⟨1, 1⟩})
94	93	eleq1d 2813	. . . . . . . 8 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨0, 1⟩, ⟨1, 1⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
95	93	eqeq1d 2731	. . . . . . . . . 10 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
96	93	eqeq1d 2731	. . . . . . . . . 10 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
97	93	eqeq1d 2731	. . . . . . . . . 10 ⊢ (𝑋 = 1 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨0, 1⟩, ⟨1, 1⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
98	95, 96, 97	3orbi123d 1437	. . . . . . . . 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 3153	. . . . . . . 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 632	. . . . . . 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 857	. . . . 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 4601	. . . . 5 ⊢ (𝑋 ∈ {2, 3} → (𝑋 = 2 ∨ 𝑋 = 3))
105	65, 11	opelxpd 5658	. . . . . . . . . . . 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 5390	. . . . . . . . . 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 2740	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
111	30	eqeq2d 2740	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ({⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
112	33	eqeq2d 2740	. . . . . . . . . . . 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 1437	. . . . . . . . . . 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 4684	. . . . . . . . . . . . 13 ⊢ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 0⟩, ⟨1, 1⟩}
115	41	opeq2d 4831	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨1, 1⟩ = ⟨1, ((0 + 1) mod 𝑁)⟩)
116	115	preq2d 4692	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨1, 0⟩, ⟨1, 1⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})
117	114, 116	eqtrid 2776	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 0⟩, ⟨1, ((0 + 1) mod 𝑁)⟩})
118	117	3mix3d 1339	. . . . . . . . . . 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 3580	. . . . . . . . . 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 6822	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → (𝐹‘𝑋) = (𝐹‘2))
123	48	fveq1i 6823	. . . . . . . . . . . . 13 ⊢ (𝐹‘2) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘2)
124		prex 5376	. . . . . . . . . . . . . 14 ⊢ {⟨1, 1⟩, ⟨1, 0⟩} ∈ V
125		s4fv2 14804	. . . . . . . . . . . . . 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 2752	. . . . . . . . . . . 12 ⊢ (𝐹‘2) = {⟨1, 1⟩, ⟨1, 0⟩}
128	122, 127	eqtrdi 2780	. . . . . . . . . . 11 ⊢ (𝑋 = 2 → (𝐹‘𝑋) = {⟨1, 1⟩, ⟨1, 0⟩})
129	128	eleq1d 2813	. . . . . . . . . 10 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨1, 1⟩, ⟨1, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
130	128	eqeq1d 2731	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
131	128	eqeq1d 2731	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
132	128	eqeq1d 2731	. . . . . . . . . . . 12 ⊢ (𝑋 = 2 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 1⟩, ⟨1, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
133	130, 131, 132	3orbi123d 1437	. . . . . . . . . . 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 3153	. . . . . . . . . 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 632	. . . . . . . . 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 5390	. . . . . . . . 9 ⊢ ((⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁)) ∧ ⟨0, 0⟩ ∈ ({0, 1} × (0..^𝑁))) → {⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
140	105, 12, 139	syl2anc 584	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → {⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁)))
141	27	eqeq2d 2740	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨0, ((0 + 1) mod 𝑁)⟩}))
142	30	eqeq2d 2740	. . . . . . . . . 10 ⊢ (𝑥 = 0 → ({⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩}))
143	33	eqeq2d 2740	. . . . . . . . . 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 1437	. . . . . . . . 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 4684	. . . . . . . . . . 11 ⊢ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 0⟩, ⟨1, 0⟩}
146	145	3mix2i 1335	. . . . . . . . . 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 3580	. . . . . . . 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 6822	. . . . . . . . . 10 ⊢ (𝑋 = 3 → (𝐹‘𝑋) = (𝐹‘3))
151	48	fveq1i 6823	. . . . . . . . . . 11 ⊢ (𝐹‘3) = (⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩‘3)
152		prex 5376	. . . . . . . . . . . 12 ⊢ {⟨1, 0⟩, ⟨0, 0⟩} ∈ V
153		s4fv3 14805	. . . . . . . . . . . 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 2752	. . . . . . . . . 10 ⊢ (𝐹‘3) = {⟨1, 0⟩, ⟨0, 0⟩}
156	150, 155	eqtrdi 2780	. . . . . . . . 9 ⊢ (𝑋 = 3 → (𝐹‘𝑋) = {⟨1, 0⟩, ⟨0, 0⟩})
157	156	eleq1d 2813	. . . . . . . 8 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ↔ {⟨1, 0⟩, ⟨0, 0⟩} ∈ 𝒫 ({0, 1} × (0..^𝑁))))
158	156	eqeq1d 2731	. . . . . . . . . 10 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩}))
159	156	eqeq1d 2731	. . . . . . . . . 10 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩}))
160	156	eqeq1d 2731	. . . . . . . . . 10 ⊢ (𝑋 = 3 → ((𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩} ↔ {⟨1, 0⟩, ⟨0, 0⟩} = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩}))
161	158, 159, 160	3orbi123d 1437	. . . . . . . . 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 3153	. . . . . . . 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 632	. . . . . . 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 857	. . . . 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 857	. . 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 847 ∨ w3o 1085 = wceq 1540 ∈ wcel 2109 ∃wrex 3053 Vcvv 3436 ∪ cun 3901 𝒫 cpw 4551 {cpr 4579 ⟨cop 4583 class class class wbr 5092 × cxp 5617 ‘cfv 6482 (class class class)co 7349 ℝcr 11008 0cc0 11009 1c1 11010 + caddc 11012 < clt 11149 ℕcn 12128 2c2 12183 3c3 12184 4c4 12185 ℕ₀cn0 12384 ℤ_≥cuz 12735 ..^cfzo 13557 mod cmo 13773 ⟨“cs4 14750

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-er 8625 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-sup 9332 df-inf 9333 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-n0 12385 df-z 12472 df-uz 12736 df-rp 12894 df-fz 13411 df-fzo 13558 df-fl 13696 df-mod 13774 df-hash 14238 df-word 14421 df-concat 14478 df-s1 14503 df-s2 14755 df-s3 14756 df-s4 14757

This theorem is referenced by: gpgprismgr4cycllem10 48098

W3C validator