spfinex - New Foundations Explorer

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

Theorem spfinex 4537

Description: Sp_fin is a set. (Contributed by SF, 20-Jan-2015.)

**Assertion**
Ref	Expression
spfinex	⊢ Sp_fin ∈ V

Proof of Theorem spfinex Dummy variables x a z t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-spfin 4447	. . 3 ⊢ Sp_fin = ∩{a ∣ ( Nc_fin V ∈ a ∧ ∀x ∈ a ∀z( S_fin (z, x) → z ∈ a))}
2		vex 2862	. . . . . . . . . . . 12 ⊢ a ∈ V
3	2	elimak 4259	. . . . . . . . . . 11 ⊢ (a ∈ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c) ↔ ∃t ∈ 1_c ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)))
4		el1c 4139	. . . . . . . . . . . . . . 15 ⊢ (t ∈ 1_c ↔ ∃x t = {x})
5	4	anbi1i 676	. . . . . . . . . . . . . 14 ⊢ ((t ∈ 1_c ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ (∃x t = {x} ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
6		19.41v 1901	. . . . . . . . . . . . . 14 ⊢ (∃x(t = {x} ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ (∃x t = {x} ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
7	5, 6	bitr4i 243	. . . . . . . . . . . . 13 ⊢ ((t ∈ 1_c ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ ∃x(t = {x} ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
8	7	exbii 1582	. . . . . . . . . . . 12 ⊢ (∃t(t ∈ 1_c ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ ∃t∃x(t = {x} ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
9		df-rex 2620	. . . . . . . . . . . 12 ⊢ (∃t ∈ 1_c ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ↔ ∃t(t ∈ 1_c ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
10		excom 1741	. . . . . . . . . . . 12 ⊢ (∃x∃t(t = {x} ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ ∃t∃x(t = {x} ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
11	8, 9, 10	3bitr4i 268	. . . . . . . . . . 11 ⊢ (∃t ∈ 1_c ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ↔ ∃x∃t(t = {x} ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
12		snex 4111	. . . . . . . . . . . . . 14 ⊢ {x} ∈ V
13		opkeq1 4059	. . . . . . . . . . . . . . 15 ⊢ (t = {x} → ⟪t, a⟫ = ⟪{x}, a⟫)
14	13	eleq1d 2419	. . . . . . . . . . . . . 14 ⊢ (t = {x} → (⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ↔ ⟪{x}, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
15	12, 14	ceqsexv 2894	. . . . . . . . . . . . 13 ⊢ (∃t(t = {x} ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ ⟪{x}, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)))
16		elin 3219	. . . . . . . . . . . . 13 ⊢ (⟪{x}, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ↔ (⟪{x}, a⟫ ∈ S_k ∧ ⟪{x}, a⟫ ∈ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)))
17		vex 2862	. . . . . . . . . . . . . . 15 ⊢ x ∈ V
18	17, 2	elssetk 4270	. . . . . . . . . . . . . 14 ⊢ (⟪{x}, a⟫ ∈ S_k ↔ x ∈ a)
19		opkex 4113	. . . . . . . . . . . . . . . . 17 ⊢ ⟪{x}, a⟫ ∈ V
20	19	elimak 4259	. . . . . . . . . . . . . . . 16 ⊢ (⟪{x}, a⟫ ∈ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ))
21		df-rex 2620	. . . . . . . . . . . . . . . 16 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )))
22		elpw121c 4148	. . . . . . . . . . . . . . . . . . . 20 ⊢ (t ∈ ℘₁℘₁1_c ↔ ∃z t = {{{z}}})
23	22	anbi1i 676	. . . . . . . . . . . . . . . . . . 19 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )) ↔ (∃z t = {{{z}}} ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )))
24		19.41v 1901	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃z(t = {{{z}}} ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )) ↔ (∃z t = {{{z}}} ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )))
25	23, 24	bitr4i 243	. . . . . . . . . . . . . . . . . 18 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )) ↔ ∃z(t = {{{z}}} ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )))
26	25	exbii 1582	. . . . . . . . . . . . . . . . 17 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )) ↔ ∃t∃z(t = {{{z}}} ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )))
27		excom 1741	. . . . . . . . . . . . . . . . 17 ⊢ (∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )) ↔ ∃t∃z(t = {{{z}}} ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )))
28	26, 27	bitr4i 243	. . . . . . . . . . . . . . . 16 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )) ↔ ∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )))
29	20, 21, 28	3bitri 262	. . . . . . . . . . . . . . 15 ⊢ (⟪{x}, a⟫ ∈ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )))
30		snex 4111	. . . . . . . . . . . . . . . . . 18 ⊢ {{{z}}} ∈ V
31		opkeq1 4059	. . . . . . . . . . . . . . . . . . 19 ⊢ (t = {{{z}}} → ⟪t, ⟪{x}, a⟫⟫ = ⟪{{{z}}}, ⟪{x}, a⟫⟫)
32	31	eleq1d 2419	. . . . . . . . . . . . . . . . . 18 ⊢ (t = {{{z}}} → (⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) ↔ ⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )))
33	30, 32	ceqsexv 2894	. . . . . . . . . . . . . . . . 17 ⊢ (∃t(t = {{{z}}} ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )) ↔ ⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ))
34		eldif 3221	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) ↔ (⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∧ ¬ ⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins2_k S_k ))
35		snex 4111	. . . . . . . . . . . . . . . . . . . 20 ⊢ {z} ∈ V
36	35, 12, 2	otkelins3k 4256	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ↔ ⟪{z}, {x}⟫ ∈ SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)))
37		vex 2862	. . . . . . . . . . . . . . . . . . . 20 ⊢ z ∈ V
38	37, 17	opksnelsik 4265	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{z}, {x}⟫ ∈ SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ↔ ⟪z, x⟫ ∈ (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)))
39	37, 17	srelk 4524	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪z, x⟫ ∈ (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ↔ S_fin (z, x))
40	36, 38, 39	3bitri 262	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ↔ S_fin (z, x))
41	35, 12, 2	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins2_k S_k ↔ ⟪{z}, a⟫ ∈ S_k )
42	37, 2	elssetk 4270	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{z}, a⟫ ∈ S_k ↔ z ∈ a)
43	41, 42	bitri 240	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins2_k S_k ↔ z ∈ a)
44	43	notbii 287	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins2_k S_k ↔ ¬ z ∈ a)
45	40, 44	anbi12i 678	. . . . . . . . . . . . . . . . 17 ⊢ ((⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∧ ¬ ⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins2_k S_k ) ↔ ( S_fin (z, x) ∧ ¬ z ∈ a))
46	33, 34, 45	3bitri 262	. . . . . . . . . . . . . . . 16 ⊢ (∃t(t = {{{z}}} ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )) ↔ ( S_fin (z, x) ∧ ¬ z ∈ a))
47	46	exbii 1582	. . . . . . . . . . . . . . 15 ⊢ (∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k )) ↔ ∃z( S_fin (z, x) ∧ ¬ z ∈ a))
48		exanali 1585	. . . . . . . . . . . . . . 15 ⊢ (∃z( S_fin (z, x) ∧ ¬ z ∈ a) ↔ ¬ ∀z( S_fin (z, x) → z ∈ a))
49	29, 47, 48	3bitri 262	. . . . . . . . . . . . . 14 ⊢ (⟪{x}, a⟫ ∈ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ¬ ∀z( S_fin (z, x) → z ∈ a))
50	18, 49	anbi12i 678	. . . . . . . . . . . . 13 ⊢ ((⟪{x}, a⟫ ∈ S_k ∧ ⟪{x}, a⟫ ∈ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ↔ (x ∈ a ∧ ¬ ∀z( S_fin (z, x) → z ∈ a)))
51	15, 16, 50	3bitri 262	. . . . . . . . . . . 12 ⊢ (∃t(t = {x} ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ (x ∈ a ∧ ¬ ∀z( S_fin (z, x) → z ∈ a)))
52	51	exbii 1582	. . . . . . . . . . 11 ⊢ (∃x∃t(t = {x} ∧ ⟪t, a⟫ ∈ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ ∃x(x ∈ a ∧ ¬ ∀z( S_fin (z, x) → z ∈ a)))
53	3, 11, 52	3bitri 262	. . . . . . . . . 10 ⊢ (a ∈ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c) ↔ ∃x(x ∈ a ∧ ¬ ∀z( S_fin (z, x) → z ∈ a)))
54		df-rex 2620	. . . . . . . . . 10 ⊢ (∃x ∈ a ¬ ∀z( S_fin (z, x) → z ∈ a) ↔ ∃x(x ∈ a ∧ ¬ ∀z( S_fin (z, x) → z ∈ a)))
55	53, 54	bitr4i 243	. . . . . . . . 9 ⊢ (a ∈ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c) ↔ ∃x ∈ a ¬ ∀z( S_fin (z, x) → z ∈ a))
56	55	notbii 287	. . . . . . . 8 ⊢ (¬ a ∈ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c) ↔ ¬ ∃x ∈ a ¬ ∀z( S_fin (z, x) → z ∈ a))
57	2	elcompl 3225	. . . . . . . 8 ⊢ (a ∈ ∼ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c) ↔ ¬ a ∈ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c))
58		dfral2 2626	. . . . . . . 8 ⊢ (∀x ∈ a ∀z( S_fin (z, x) → z ∈ a) ↔ ¬ ∃x ∈ a ¬ ∀z( S_fin (z, x) → z ∈ a))
59	56, 57, 58	3bitr4i 268	. . . . . . 7 ⊢ (a ∈ ∼ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c) ↔ ∀x ∈ a ∀z( S_fin (z, x) → z ∈ a))
60	59	abbi2i 2464	. . . . . 6 ⊢ ∼ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c) = {a ∣ ∀x ∈ a ∀z( S_fin (z, x) → z ∈ a)}
61	60	ineq2i 3454	. . . . 5 ⊢ ({a ∣ Nc_fin V ∈ a} ∩ ∼ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c)) = ({a ∣ Nc_fin V ∈ a} ∩ {a ∣ ∀x ∈ a ∀z( S_fin (z, x) → z ∈ a)})
62		inab 3522	. . . . 5 ⊢ ({a ∣ Nc_fin V ∈ a} ∩ {a ∣ ∀x ∈ a ∀z( S_fin (z, x) → z ∈ a)}) = {a ∣ ( Nc_fin V ∈ a ∧ ∀x ∈ a ∀z( S_fin (z, x) → z ∈ a))}
63	61, 62	eqtri 2373	. . . 4 ⊢ ({a ∣ Nc_fin V ∈ a} ∩ ∼ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c)) = {a ∣ ( Nc_fin V ∈ a ∧ ∀x ∈ a ∀z( S_fin (z, x) → z ∈ a))}
64	63	inteqi 3930	. . 3 ⊢ ∩({a ∣ Nc_fin V ∈ a} ∩ ∼ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c)) = ∩{a ∣ ( Nc_fin V ∈ a ∧ ∀x ∈ a ∀z( S_fin (z, x) → z ∈ a))}
65	1, 64	eqtr4i 2376	. 2 ⊢ Sp_fin = ∩({a ∣ Nc_fin V ∈ a} ∩ ∼ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c))
66		setswithex 4322	. . . 4 ⊢ {a ∣ Nc_fin V ∈ a} ∈ V
67		ssetkex 4294	. . . . . . 7 ⊢ S_k ∈ V
68		srelkex 4525	. . . . . . . . . . 11 ⊢ (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∈ V
69	68	sikex 4297	. . . . . . . . . 10 ⊢ SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∈ V
70	69	ins3kex 4308	. . . . . . . . 9 ⊢ Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∈ V
71	67	ins2kex 4307	. . . . . . . . 9 ⊢ Ins2_k S_k ∈ V
72	70, 71	difex 4107	. . . . . . . 8 ⊢ ( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) ∈ V
73		1cex 4142	. . . . . . . . . 10 ⊢ 1_c ∈ V
74	73	pw1ex 4303	. . . . . . . . 9 ⊢ ℘₁1_c ∈ V
75	74	pw1ex 4303	. . . . . . . 8 ⊢ ℘₁℘₁1_c ∈ V
76	72, 75	imakex 4300	. . . . . . 7 ⊢ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∈ V
77	67, 76	inex 4105	. . . . . 6 ⊢ ( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ∈ V
78	77, 73	imakex 4300	. . . . 5 ⊢ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c) ∈ V
79	78	complex 4104	. . . 4 ⊢ ∼ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c) ∈ V
80	66, 79	inex 4105	. . 3 ⊢ ({a ∣ Nc_fin V ∈ a} ∩ ∼ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c)) ∈ V
81	80	intex 4320	. 2 ⊢ ∩({a ∣ Nc_fin V ∈ a} ∩ ∼ (( S_k ∩ (( Ins3_k SI_k (( Nn ×_k Nn ) ∩ (( Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∖ Ins2_k S_k ) “_k ℘₁℘₁1_c)) “_k 1_c)) ∈ V
82	65, 81	eqeltri 2423	1 ⊢ Sp_fin ∈ V

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 358 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 {cab 2339 ∀wral 2614 ∃wrex 2615 Vcvv 2859 ∼ ccompl 3205 ∖ cdif 3206 ∩ cin 3208 ⊕ csymdif 3209 ℘cpw 3722 {csn 3737 ∩cint 3926 ⟪copk 4057 1_cc1c 4134 ℘₁cpw1 4135 ×_k cxpk 4174 Ins2_k cins2k 4176 Ins3_k cins3k 4177 “_k cimak 4179 SI_k csik 4181 S_k cssetk 4183 Nn cnnc 4373 Nc_fin cncfin 4434 S_fin wsfin 4438 Sp_fin cspfin 4439

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 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 4078 ax-xp 4079 ax-cnv 4080 ax-1c 4081 ax-sset 4082 ax-si 4083 ax-ins2 4084 ax-ins3 4085 ax-typlower 4086 ax-sn 4087

This theorem 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 2478 df-ne 2518 df-ral 2619 df-rex 2620 df-v 2861 df-sbc 3047 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-symdif 3216 df-ss 3259 df-nul 3551 df-if 3663 df-pw 3724 df-sn 3741 df-pr 3742 df-uni 3892 df-int 3927 df-opk 4058 df-1c 4136 df-pw1 4137 df-uni1 4138 df-xpk 4185 df-cnvk 4186 df-ins2k 4187 df-ins3k 4188 df-imak 4189 df-cok 4190 df-p6 4191 df-sik 4192 df-ssetk 4193 df-imagek 4194 df-addc 4378 df-nnc 4379 df-sfin 4446 df-spfin 4447

This theorem is referenced by: spfininduct 4540 vfinspss 4551 vfinspclt 4552 vfinncsp 4554 vinf 4555

W3C validator