spfinex - New Foundations Explorer

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

Theorem spfinex 4538

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 4448	. . 3 ⊢ Sp_fin = ∩{a ∣ ( Nc_fin V ∈ a ∧ ∀x ∈ a ∀z( S_fin (z, x) → z ∈ a))}
2		vex 2863	. . . . . . . . . . . 12 ⊢ a ∈ V
3	2	elimak 4260	. . . . . . . . . . 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 4140	. . . . . . . . . . . . . . 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 2621	. . . . . . . . . . . 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 4112	. . . . . . . . . . . . . 14 ⊢ {x} ∈ V
13		opkeq1 4060	. . . . . . . . . . . . . . 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 2895	. . . . . . . . . . . . 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 3220	. . . . . . . . . . . . 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 2863	. . . . . . . . . . . . . . 15 ⊢ x ∈ V
18	17, 2	elssetk 4271	. . . . . . . . . . . . . 14 ⊢ (⟪{x}, a⟫ ∈ S_k ↔ x ∈ a)
19		opkex 4114	. . . . . . . . . . . . . . . . 17 ⊢ ⟪{x}, a⟫ ∈ V
20	19	elimak 4260	. . . . . . . . . . . . . . . 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 2621	. . . . . . . . . . . . . . . 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 4149	. . . . . . . . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . . . . . . 18 ⊢ {{{z}}} ∈ V
31		opkeq1 4060	. . . . . . . . . . . . . . . . . . 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 2895	. . . . . . . . . . . . . . . . 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 3222	. . . . . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . . . . . . . . 20 ⊢ {z} ∈ V
36	35, 12, 2	otkelins3k 4257	. . . . . . . . . . . . . . . . . . 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 2863	. . . . . . . . . . . . . . . . . . . 20 ⊢ z ∈ V
38	37, 17	opksnelsik 4266	. . . . . . . . . . . . . . . . . . 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 4525	. . . . . . . . . . . . . . . . . . 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 4256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins2_k S_k ↔ ⟪{z}, a⟫ ∈ S_k )
42	37, 2	elssetk 4271	. . . . . . . . . . . . . . . . . . . 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 2621	. . . . . . . . . 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 3226	. . . . . . . 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 2627	. . . . . . . 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	eqabi 2465	. . . . . 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 3455	. . . . 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 3523	. . . . 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 3931	. . 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 4323	. . . 4 ⊢ {a ∣ Nc_fin V ∈ a} ∈ V
67		ssetkex 4295	. . . . . . 7 ⊢ S_k ∈ V
68		srelkex 4526	. . . . . . . . . . 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 4298	. . . . . . . . . 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 4309	. . . . . . . . 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 4308	. . . . . . . . 9 ⊢ Ins2_k S_k ∈ V
72	70, 71	difex 4108	. . . . . . . 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 4143	. . . . . . . . . 10 ⊢ 1_c ∈ V
74	73	pw1ex 4304	. . . . . . . . 9 ⊢ 𝒫₁1_c ∈ V
75	74	pw1ex 4304	. . . . . . . 8 ⊢ 𝒫₁𝒫₁1_c ∈ V
76	72, 75	imakex 4301	. . . . . . 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 4106	. . . . . 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 4301	. . . . 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 4105	. . . 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 4106	. . 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 4321	. 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

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 358 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 {cab 2339 ∀wral 2615 ∃wrex 2616 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ∩ cin 3209 ⊕ csymdif 3210 𝒫 cpw 3723 {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 SI_k csik 4182 S_k cssetk 4184 Nn cnnc 4374 Nc_fin cncfin 4435 S_fin wsfin 4439 Sp_fin cspfin 4440

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-xp 4080 ax-cnv 4081 ax-1c 4082 ax-sset 4083 ax-si 4084 ax-ins2 4085 ax-ins3 4086 ax-typlower 4087 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-sbc 3048 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-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-uni1 4139 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-p6 4192 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-addc 4379 df-nnc 4380 df-sfin 4447 df-spfin 4448

This theorem is used by: spfininduct 4541 vfinspss 4552 vfinspclt 4553 vfinncsp 4555 vinf 4556

W3C validator