dfnnc2 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > dfnnc2		GIF version

Theorem dfnnc2 4396

Description: Definition of the finite cardinals for existence theorem. (Contributed by SF, 14-Jan-2015.)

**Assertion**
Ref	Expression
dfnnc2	⊢ Nn = ∩({x ∣ 0_c ∈ x} ∖ (( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 1_c))

Proof of Theorem dfnnc2 Dummy variables y z w t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-nnc 4380	. 2 ⊢ Nn = ∩{y ∣ (0_c ∈ y ∧ ∀z ∈ y (z +_c 1_c) ∈ y)}
2		eldif 3222	. . . . 5 ⊢ (y ∈ ({x ∣ 0_c ∈ x} ∖ (( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 1_c)) ↔ (y ∈ {x ∣ 0_c ∈ x} ∧ ¬ y ∈ (( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 1_c)))
3		vex 2863	. . . . . . 7 ⊢ y ∈ V
4		eleq2 2414	. . . . . . 7 ⊢ (x = y → (0_c ∈ x ↔ 0_c ∈ y))
5	3, 4	elab 2986	. . . . . 6 ⊢ (y ∈ {x ∣ 0_c ∈ x} ↔ 0_c ∈ y)
6		snex 4112	. . . . . . . . . . . 12 ⊢ {z} ∈ V
7		opkeq1 4060	. . . . . . . . . . . . 13 ⊢ (t = {z} → ⟪t, y⟫ = ⟪{z}, y⟫)
8	7	eleq1d 2419	. . . . . . . . . . . 12 ⊢ (t = {z} → (⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) ↔ ⟪{z}, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))))
9	6, 8	ceqsexv 2895	. . . . . . . . . . 11 ⊢ (∃t(t = {z} ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))) ↔ ⟪{z}, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))))
10		eldif 3222	. . . . . . . . . . . 12 ⊢ (⟪{z}, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) ↔ (⟪{z}, y⟫ ∈ S_k ∧ ¬ ⟪{z}, y⟫ ∈ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))))
11		vex 2863	. . . . . . . . . . . . . 14 ⊢ z ∈ V
12	11, 3	elssetk 4271	. . . . . . . . . . . . 13 ⊢ (⟪{z}, y⟫ ∈ S_k ↔ z ∈ y)
13		snex 4112	. . . . . . . . . . . . . . . . . 18 ⊢ {w} ∈ V
14		opkeq2 4061	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (t = {w} → ⟪{z}, t⟫ = ⟪{z}, {w}⟫)
15	14	eleq1d 2419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (t = {w} → (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ↔ ⟪{z}, {w}⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))
16		vex 2863	. . . . . . . . . . . . . . . . . . . . 21 ⊢ w ∈ V
17	11, 16	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{z}, {w}⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ↔ ⟪z, w⟫ ∈ Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))
18	15, 17	syl6bb 252	. . . . . . . . . . . . . . . . . . 19 ⊢ (t = {w} → (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ↔ ⟪z, w⟫ ∈ Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))
19		opkeq1 4060	. . . . . . . . . . . . . . . . . . . 20 ⊢ (t = {w} → ⟪t, y⟫ = ⟪{w}, y⟫)
20	19	eleq1d 2419	. . . . . . . . . . . . . . . . . . 19 ⊢ (t = {w} → (⟪t, y⟫ ∈ S_k ↔ ⟪{w}, y⟫ ∈ S_k ))
21	18, 20	anbi12d 691	. . . . . . . . . . . . . . . . . 18 ⊢ (t = {w} → ((⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k ) ↔ (⟪z, w⟫ ∈ Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪{w}, y⟫ ∈ S_k )))
22	13, 21	ceqsexv 2895	. . . . . . . . . . . . . . . . 17 ⊢ (∃t(t = {w} ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )) ↔ (⟪z, w⟫ ∈ Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪{w}, y⟫ ∈ S_k ))
23		opkelimagekg 4272	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((z ∈ V ∧ w ∈ V) → (⟪z, w⟫ ∈ Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ↔ w = ((( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) “_k z)))
24	11, 16, 23	mp2an 653	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪z, w⟫ ∈ Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ↔ w = ((( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) “_k z))
25		dfaddc2 4382	. . . . . . . . . . . . . . . . . . . 20 ⊢ (z +_c 1_c) = ((( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) “_k z)
26	25	eqeq2i 2363	. . . . . . . . . . . . . . . . . . 19 ⊢ (w = (z +_c 1_c) ↔ w = ((( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) “_k z))
27	24, 26	bitr4i 243	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪z, w⟫ ∈ Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ↔ w = (z +_c 1_c))
28	16, 3	elssetk 4271	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪{w}, y⟫ ∈ S_k ↔ w ∈ y)
29	27, 28	anbi12i 678	. . . . . . . . . . . . . . . . 17 ⊢ ((⟪z, w⟫ ∈ Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪{w}, y⟫ ∈ S_k ) ↔ (w = (z +_c 1_c) ∧ w ∈ y))
30	22, 29	bitri 240	. . . . . . . . . . . . . . . 16 ⊢ (∃t(t = {w} ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )) ↔ (w = (z +_c 1_c) ∧ w ∈ y))
31	30	exbii 1582	. . . . . . . . . . . . . . 15 ⊢ (∃w∃t(t = {w} ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )) ↔ ∃w(w = (z +_c 1_c) ∧ w ∈ y))
32	6, 3	opkelcok 4263	. . . . . . . . . . . . . . . 16 ⊢ (⟪{z}, y⟫ ∈ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)) ↔ ∃t(⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k ))
33		el1c 4140	. . . . . . . . . . . . . . . . . . . 20 ⊢ (t ∈ 1_c ↔ ∃w t = {w})
34	33	anbi1i 676	. . . . . . . . . . . . . . . . . . 19 ⊢ ((t ∈ 1_c ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )) ↔ (∃w t = {w} ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )))
35		19.41v 1901	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃w(t = {w} ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )) ↔ (∃w t = {w} ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )))
36	34, 35	bitr4i 243	. . . . . . . . . . . . . . . . . 18 ⊢ ((t ∈ 1_c ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )) ↔ ∃w(t = {w} ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )))
37	36	exbii 1582	. . . . . . . . . . . . . . . . 17 ⊢ (∃t(t ∈ 1_c ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )) ↔ ∃t∃w(t = {w} ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )))
38		sikss1c1c 4268	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ⊆ (1_c ×_k 1_c)
39	38	sseli 3270	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) → ⟪{z}, t⟫ ∈ (1_c ×_k 1_c))
40		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ t ∈ V
41	6, 40	opkelxpk 4249	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪{z}, t⟫ ∈ (1_c ×_k 1_c) ↔ ({z} ∈ 1_c ∧ t ∈ 1_c))
42	41	simprbi 450	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟪{z}, t⟫ ∈ (1_c ×_k 1_c) → t ∈ 1_c)
43	39, 42	syl 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) → t ∈ 1_c)
44	43	pm4.71ri 614	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ↔ (t ∈ 1_c ∧ ⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))
45	44	anbi1i 676	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k ) ↔ ((t ∈ 1_c ∧ ⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)) ∧ ⟪t, y⟫ ∈ S_k ))
46		anass 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (((t ∈ 1_c ∧ ⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)) ∧ ⟪t, y⟫ ∈ S_k ) ↔ (t ∈ 1_c ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )))
47	45, 46	bitri 240	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k ) ↔ (t ∈ 1_c ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )))
48	47	exbii 1582	. . . . . . . . . . . . . . . . 17 ⊢ (∃t(⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k ) ↔ ∃t(t ∈ 1_c ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )))
49		excom 1741	. . . . . . . . . . . . . . . . 17 ⊢ (∃w∃t(t = {w} ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )) ↔ ∃t∃w(t = {w} ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )))
50	37, 48, 49	3bitr4i 268	. . . . . . . . . . . . . . . 16 ⊢ (∃t(⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k ) ↔ ∃w∃t(t = {w} ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )))
51	32, 50	bitri 240	. . . . . . . . . . . . . . 15 ⊢ (⟪{z}, y⟫ ∈ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)) ↔ ∃w∃t(t = {w} ∧ (⟪{z}, t⟫ ∈ SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∧ ⟪t, y⟫ ∈ S_k )))
52		df-clel 2349	. . . . . . . . . . . . . . 15 ⊢ ((z +_c 1_c) ∈ y ↔ ∃w(w = (z +_c 1_c) ∧ w ∈ y))
53	31, 51, 52	3bitr4i 268	. . . . . . . . . . . . . 14 ⊢ (⟪{z}, y⟫ ∈ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)) ↔ (z +_c 1_c) ∈ y)
54	53	notbii 287	. . . . . . . . . . . . 13 ⊢ (¬ ⟪{z}, y⟫ ∈ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)) ↔ ¬ (z +_c 1_c) ∈ y)
55	12, 54	anbi12i 678	. . . . . . . . . . . 12 ⊢ ((⟪{z}, y⟫ ∈ S_k ∧ ¬ ⟪{z}, y⟫ ∈ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) ↔ (z ∈ y ∧ ¬ (z +_c 1_c) ∈ y))
56	10, 55	bitri 240	. . . . . . . . . . 11 ⊢ (⟪{z}, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) ↔ (z ∈ y ∧ ¬ (z +_c 1_c) ∈ y))
57	9, 56	bitri 240	. . . . . . . . . 10 ⊢ (∃t(t = {z} ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))) ↔ (z ∈ y ∧ ¬ (z +_c 1_c) ∈ y))
58	57	exbii 1582	. . . . . . . . 9 ⊢ (∃z∃t(t = {z} ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))) ↔ ∃z(z ∈ y ∧ ¬ (z +_c 1_c) ∈ y))
59	3	elimak 4260	. . . . . . . . . 10 ⊢ (y ∈ (( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 1_c) ↔ ∃t ∈ 1_c ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))))
60		el1c 4140	. . . . . . . . . . . . . 14 ⊢ (t ∈ 1_c ↔ ∃z t = {z})
61	60	anbi1i 676	. . . . . . . . . . . . 13 ⊢ ((t ∈ 1_c ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))) ↔ (∃z t = {z} ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))))
62		19.41v 1901	. . . . . . . . . . . . 13 ⊢ (∃z(t = {z} ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))) ↔ (∃z t = {z} ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))))
63	61, 62	bitr4i 243	. . . . . . . . . . . 12 ⊢ ((t ∈ 1_c ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))) ↔ ∃z(t = {z} ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))))
64	63	exbii 1582	. . . . . . . . . . 11 ⊢ (∃t(t ∈ 1_c ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))) ↔ ∃t∃z(t = {z} ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))))
65		df-rex 2621	. . . . . . . . . . 11 ⊢ (∃t ∈ 1_c ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) ↔ ∃t(t ∈ 1_c ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))))
66		excom 1741	. . . . . . . . . . 11 ⊢ (∃z∃t(t = {z} ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))) ↔ ∃t∃z(t = {z} ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))))
67	64, 65, 66	3bitr4i 268	. . . . . . . . . 10 ⊢ (∃t ∈ 1_c ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) ↔ ∃z∃t(t = {z} ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))))
68	59, 67	bitri 240	. . . . . . . . 9 ⊢ (y ∈ (( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 1_c) ↔ ∃z∃t(t = {z} ∧ ⟪t, y⟫ ∈ ( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c)))))
69		df-rex 2621	. . . . . . . . 9 ⊢ (∃z ∈ y ¬ (z +_c 1_c) ∈ y ↔ ∃z(z ∈ y ∧ ¬ (z +_c 1_c) ∈ y))
70	58, 68, 69	3bitr4i 268	. . . . . . . 8 ⊢ (y ∈ (( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 1_c) ↔ ∃z ∈ y ¬ (z +_c 1_c) ∈ y)
71		rexnal 2626	. . . . . . . 8 ⊢ (∃z ∈ y ¬ (z +_c 1_c) ∈ y ↔ ¬ ∀z ∈ y (z +_c 1_c) ∈ y)
72	70, 71	bitr2i 241	. . . . . . 7 ⊢ (¬ ∀z ∈ y (z +_c 1_c) ∈ y ↔ y ∈ (( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 1_c))
73	72	con1bii 321	. . . . . 6 ⊢ (¬ y ∈ (( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 1_c) ↔ ∀z ∈ y (z +_c 1_c) ∈ y)
74	5, 73	anbi12i 678	. . . . 5 ⊢ ((y ∈ {x ∣ 0_c ∈ x} ∧ ¬ y ∈ (( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 1_c)) ↔ (0_c ∈ y ∧ ∀z ∈ y (z +_c 1_c) ∈ y))
75	2, 74	bitri 240	. . . 4 ⊢ (y ∈ ({x ∣ 0_c ∈ x} ∖ (( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 1_c)) ↔ (0_c ∈ y ∧ ∀z ∈ y (z +_c 1_c) ∈ y))
76	75	eqabi 2465	. . 3 ⊢ ({x ∣ 0_c ∈ x} ∖ (( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 1_c)) = {y ∣ (0_c ∈ y ∧ ∀z ∈ y (z +_c 1_c) ∈ y)}
77	76	inteqi 3931	. 2 ⊢ ∩({x ∣ 0_c ∈ x} ∖ (( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 1_c)) = ∩{y ∣ (0_c ∈ y ∧ ∀z ∈ y (z +_c 1_c) ∈ y)}
78	1, 77	eqtr4i 2376	1 ⊢ Nn = ∩({x ∣ 0_c ∈ x} ∖ (( S_k ∖ ( S_k ∘_k SI_k Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 1_c))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 ↔ wb 176 ∧ wa 358 ∃wex 1541 = wceq 1642 ∈ wcel 1710 {cab 2339 ∀wral 2615 ∃wrex 2616 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ∪ cun 3208 ∩ cin 3209 ⊕ csymdif 3210 {csn 3738 ∩cint 3927 ⟪copk 4058 1_cc1c 4135 𝒫₁cpw1 4136 ×_k cxpk 4175 Ins2_k cins2k 4177 Ins3_k cins3k 4178 “_k cimak 4180 ∘_k ccomk 4181 SI_k csik 4182 Image_kcimagek 4183 S_k cssetk 4184 Nn cnnc 4374 0_cc0c 4375 +_c cplc 4376

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4079 ax-sn 4088

This proof depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-v 2862 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-nul 3552 df-pw 3725 df-sn 3742 df-pr 3743 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-addc 4379 df-nnc 4380

This theorem is used by: nncex 4397

W3C validator