ncfinraiselem2 - New Foundations Explorer

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

Theorem ncfinraiselem2 4481

Description: Lemma for ncfinraise 4482. Show stratification for induction. (Contributed by SF, 22-Jan-2015.)

**Assertion**
Ref	Expression
ncfinraiselem2	⊢ {m ∣ ∀a ∈ m ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n)} ∈ V

Distinct variable groups: a,b,m n,a m,b n,b

Proof of Theorem ncfinraiselem2 Dummy variables t x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		snex 4112	. . . . . 6 ⊢ {m} ∈ V
2	1	elcompl 3226	. . . . 5 ⊢ ({m} ∈ ∼ (( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) “_k ℘₁1_c) ↔ ¬ {m} ∈ (( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) “_k ℘₁1_c))
3	1	elimak 4260	. . . . . 6 ⊢ ({m} ∈ (( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) “_k ℘₁1_c) ↔ ∃t ∈ ℘₁ 1_c⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)))
4		elpw11c 4148	. . . . . . . . . 10 ⊢ (t ∈ ℘₁1_c ↔ ∃a t = {{a}})
5	4	anbi1i 676	. . . . . . . . 9 ⊢ ((t ∈ ℘₁1_c ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))) ↔ (∃a t = {{a}} ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))))
6		19.41v 1901	. . . . . . . . 9 ⊢ (∃a(t = {{a}} ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))) ↔ (∃a t = {{a}} ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))))
7	5, 6	bitr4i 243	. . . . . . . 8 ⊢ ((t ∈ ℘₁1_c ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))) ↔ ∃a(t = {{a}} ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))))
8	7	exbii 1582	. . . . . . 7 ⊢ (∃t(t ∈ ℘₁1_c ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))) ↔ ∃t∃a(t = {{a}} ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))))
9		df-rex 2621	. . . . . . 7 ⊢ (∃t ∈ ℘₁ 1_c⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ↔ ∃t(t ∈ ℘₁1_c ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))))
10		excom 1741	. . . . . . 7 ⊢ (∃a∃t(t = {{a}} ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))) ↔ ∃t∃a(t = {{a}} ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))))
11	8, 9, 10	3bitr4i 268	. . . . . 6 ⊢ (∃t ∈ ℘₁ 1_c⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ↔ ∃a∃t(t = {{a}} ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))))
12		snex 4112	. . . . . . . . . 10 ⊢ {{a}} ∈ V
13		opkeq1 4060	. . . . . . . . . . 11 ⊢ (t = {{a}} → ⟪t, {m}⟫ = ⟪{{a}}, {m}⟫)
14	13	eleq1d 2419	. . . . . . . . . 10 ⊢ (t = {{a}} → (⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ↔ ⟪{{a}}, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))))
15	12, 14	ceqsexv 2895	. . . . . . . . 9 ⊢ (∃t(t = {{a}} ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))) ↔ ⟪{{a}}, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)))
16		elin 3220	. . . . . . . . 9 ⊢ (⟪{{a}}, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ↔ (⟪{{a}}, {m}⟫ ∈ SI_k S_k ∧ ⟪{{a}}, {m}⟫ ∈ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)))
17		snex 4112	. . . . . . . . . . . 12 ⊢ {a} ∈ V
18		vex 2863	. . . . . . . . . . . 12 ⊢ m ∈ V
19	17, 18	opksnelsik 4266	. . . . . . . . . . 11 ⊢ (⟪{{a}}, {m}⟫ ∈ SI_k S_k ↔ ⟪{a}, m⟫ ∈ S_k )
20		vex 2863	. . . . . . . . . . . 12 ⊢ a ∈ V
21	20, 18	elssetk 4271	. . . . . . . . . . 11 ⊢ (⟪{a}, m⟫ ∈ S_k ↔ a ∈ m)
22	19, 21	bitri 240	. . . . . . . . . 10 ⊢ (⟪{{a}}, {m}⟫ ∈ SI_k S_k ↔ a ∈ m)
23		opkex 4114	. . . . . . . . . . . . 13 ⊢ ⟪{{a}}, {m}⟫ ∈ V
24	23	elimak 4260	. . . . . . . . . . . 12 ⊢ (⟪{{a}}, {m}⟫ ∈ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁℘₁1_c⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)))
25		df-rex 2621	. . . . . . . . . . . 12 ⊢ (∃t ∈ ℘₁ ℘₁℘₁1_c⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) ↔ ∃t(t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))))
26		elpw131c 4150	. . . . . . . . . . . . . . . 16 ⊢ (t ∈ ℘₁℘₁℘₁1_c ↔ ∃b t = {{{{b}}}})
27	26	anbi1i 676	. . . . . . . . . . . . . . 15 ⊢ ((t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))) ↔ (∃b t = {{{{b}}}} ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))))
28		19.41v 1901	. . . . . . . . . . . . . . 15 ⊢ (∃b(t = {{{{b}}}} ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))) ↔ (∃b t = {{{{b}}}} ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))))
29	27, 28	bitr4i 243	. . . . . . . . . . . . . 14 ⊢ ((t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))) ↔ ∃b(t = {{{{b}}}} ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))))
30	29	exbii 1582	. . . . . . . . . . . . 13 ⊢ (∃t(t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))) ↔ ∃t∃b(t = {{{{b}}}} ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))))
31		excom 1741	. . . . . . . . . . . . 13 ⊢ (∃b∃t(t = {{{{b}}}} ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))) ↔ ∃t∃b(t = {{{{b}}}} ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))))
32	30, 31	bitr4i 243	. . . . . . . . . . . 12 ⊢ (∃t(t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))) ↔ ∃b∃t(t = {{{{b}}}} ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))))
33	24, 25, 32	3bitri 262	. . . . . . . . . . 11 ⊢ (⟪{{a}}, {m}⟫ ∈ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c) ↔ ∃b∃t(t = {{{{b}}}} ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))))
34		snex 4112	. . . . . . . . . . . . . . 15 ⊢ {{{{b}}}} ∈ V
35		opkeq1 4060	. . . . . . . . . . . . . . . 16 ⊢ (t = {{{{b}}}} → ⟪t, ⟪{{a}}, {m}⟫⟫ = ⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫)
36	35	eleq1d 2419	. . . . . . . . . . . . . . 15 ⊢ (t = {{{{b}}}} → (⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) ↔ ⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))))
37	34, 36	ceqsexv 2895	. . . . . . . . . . . . . 14 ⊢ (∃t(t = {{{{b}}}} ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))) ↔ ⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)))
38		eldif 3222	. . . . . . . . . . . . . 14 ⊢ (⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) ↔ (⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ∈ Ins2_k SI_k S_k ∧ ¬ ⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ∈ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)))
39		snex 4112	. . . . . . . . . . . . . . . . 17 ⊢ {{b}} ∈ V
40	39, 12, 1	otkelins2k 4256	. . . . . . . . . . . . . . . 16 ⊢ (⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ∈ Ins2_k SI_k S_k ↔ ⟪{{b}}, {m}⟫ ∈ SI_k S_k )
41		snex 4112	. . . . . . . . . . . . . . . . 17 ⊢ {b} ∈ V
42	41, 18	opksnelsik 4266	. . . . . . . . . . . . . . . 16 ⊢ (⟪{{b}}, {m}⟫ ∈ SI_k S_k ↔ ⟪{b}, m⟫ ∈ S_k )
43		vex 2863	. . . . . . . . . . . . . . . . 17 ⊢ b ∈ V
44	43, 18	elssetk 4271	. . . . . . . . . . . . . . . 16 ⊢ (⟪{b}, m⟫ ∈ S_k ↔ b ∈ m)
45	40, 42, 44	3bitri 262	. . . . . . . . . . . . . . 15 ⊢ (⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ∈ Ins2_k SI_k S_k ↔ b ∈ m)
46	39, 12, 1	otkelins3k 4257	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ∈ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c) ↔ ⟪{{b}}, {{a}}⟫ ∈ (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))
47		df-rex 2621	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃t ∈ ℘₁ 1_c⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) ↔ ∃t(t ∈ ℘₁1_c ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))))
48		elpw11c 4148	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (t ∈ ℘₁1_c ↔ ∃n t = {{n}})
49	48	anbi1i 676	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((t ∈ ℘₁1_c ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))) ↔ (∃n t = {{n}} ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))))
50		19.41v 1901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃n(t = {{n}} ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))) ↔ (∃n t = {{n}} ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))))
51	49, 50	bitr4i 243	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((t ∈ ℘₁1_c ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))) ↔ ∃n(t = {{n}} ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))))
52	51	exbii 1582	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃t(t ∈ ℘₁1_c ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))) ↔ ∃t∃n(t = {{n}} ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))))
53	47, 52	bitri 240	. . . . . . . . . . . . . . . . . 18 ⊢ (∃t ∈ ℘₁ 1_c⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) ↔ ∃t∃n(t = {{n}} ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))))
54		opkex 4114	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟪{{b}}, {{a}}⟫ ∈ V
55	54	elimak 4260	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪{{b}}, {{a}}⟫ ∈ (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c) ↔ ∃t ∈ ℘₁ 1_c⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))))
56		excom 1741	. . . . . . . . . . . . . . . . . 18 ⊢ (∃n∃t(t = {{n}} ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))) ↔ ∃t∃n(t = {{n}} ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))))
57	53, 55, 56	3bitr4i 268	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{{b}}, {{a}}⟫ ∈ (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c) ↔ ∃n∃t(t = {{n}} ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))))
58		snex 4112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {{n}} ∈ V
59		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (t = {{n}} → ⟪t, ⟪{{b}}, {{a}}⟫⟫ = ⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫)
60	59	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (t = {{n}} → (⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) ↔ ⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))))
61	58, 60	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃t(t = {{n}} ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))) ↔ ⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))))
62		elin 3220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) ↔ (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ (℘₁℘₁ Nn ×_k V) ∧ ⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))))
63	58, 54	opkelxpk 4249	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ (℘₁℘₁ Nn ×_k V) ↔ ({{n}} ∈ ℘₁℘₁ Nn ∧ ⟪{{b}}, {{a}}⟫ ∈ V))
64	54, 63	mpbiran2 885	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ (℘₁℘₁ Nn ×_k V) ↔ {{n}} ∈ ℘₁℘₁ Nn )
65		snelpw1 4147	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({{n}} ∈ ℘₁℘₁ Nn ↔ {n} ∈ ℘₁ Nn )
66		snelpw1 4147	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({n} ∈ ℘₁ Nn ↔ n ∈ Nn )
67	64, 65, 66	3bitri 262	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ (℘₁℘₁ Nn ×_k V) ↔ n ∈ Nn )
68		elin 3220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)) ↔ (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∧ ⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))
69		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ n ∈ V
70	69, 39, 12	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ↔ ⟪n, {{a}}⟫ ∈ (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))
71		opkex 4114	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ⟪n, {{a}}⟫ ∈ V
72	71	elimak 4260	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟪n, {{a}}⟫ ∈ (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ))
73		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
74		elpw121c 4149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (t ∈ ℘₁℘₁1_c ↔ ∃x t = {{{x}}})
75	74	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ (∃x t = {{{x}}} ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
76		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃x(t = {{{x}}} ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ (∃x t = {{{x}}} ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
77	75, 76	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ ∃x(t = {{{x}}} ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
78	77	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ ∃t∃x(t = {{{x}}} ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
79		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃x∃t(t = {{{x}}} ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ ∃t∃x(t = {{{x}}} ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
80	78, 79	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ ∃x∃t(t = {{{x}}} ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
81	72, 73, 80	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟪n, {{a}}⟫ ∈ (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ↔ ∃x∃t(t = {{{x}}} ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
82		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {{{x}}} ∈ V
83		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (t = {{{x}}} → ⟪t, ⟪n, {{a}}⟫⟫ = ⟪{{{x}}}, ⟪n, {{a}}⟫⟫)
84	83	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (t = {{{x}}} → (⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) ↔ ⟪{{{x}}}, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
85	82, 84	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃t(t = {{{x}}} ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ ⟪{{{x}}}, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ))
86		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟪{{{x}}}, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) ↔ (⟪{{{x}}}, ⟪n, {{a}}⟫⟫ ∈ Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∧ ⟪{{{x}}}, ⟪n, {{a}}⟫⟫ ∈ Ins3_k S_k ))
87		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ {x} ∈ V
88	87, 69, 12	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟪{{{x}}}, ⟪n, {{a}}⟫⟫ ∈ Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ↔ ⟪{x}, {{a}}⟫ ∈ SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)))
89		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ x ∈ V
90	89, 17	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟪{x}, {{a}}⟫ ∈ SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ↔ ⟪x, {a}⟫ ∈ ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)))
91	89, 20	eqpw1relk 4480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟪x, {a}⟫ ∈ ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ↔ x = ℘₁a)
92	88, 90, 91	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟪{{{x}}}, ⟪n, {{a}}⟫⟫ ∈ Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ↔ x = ℘₁a)
93	87, 69, 12	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟪{{{x}}}, ⟪n, {{a}}⟫⟫ ∈ Ins3_k S_k ↔ ⟪{x}, n⟫ ∈ S_k )
94	89, 69	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟪{x}, n⟫ ∈ S_k ↔ x ∈ n)
95	93, 94	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟪{{{x}}}, ⟪n, {{a}}⟫⟫ ∈ Ins3_k S_k ↔ x ∈ n)
96	92, 95	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟪{{{x}}}, ⟪n, {{a}}⟫⟫ ∈ Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∧ ⟪{{{x}}}, ⟪n, {{a}}⟫⟫ ∈ Ins3_k S_k ) ↔ (x = ℘₁a ∧ x ∈ n))
97	85, 86, 96	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃t(t = {{{x}}} ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ (x = ℘₁a ∧ x ∈ n))
98	97	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃x∃t(t = {{{x}}} ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ ∃x(x = ℘₁a ∧ x ∈ n))
99		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (℘₁a ∈ n ↔ ∃x(x = ℘₁a ∧ x ∈ n))
100	98, 99	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃x∃t(t = {{{x}}} ∧ ⟪t, ⟪n, {{a}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ ℘₁a ∈ n)
101	70, 81, 100	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ↔ ℘₁a ∈ n)
102		opkex 4114	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ⟪n, {{b}}⟫ ∈ V
103	102	elimak 4260	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟪n, {{b}}⟫ ∈ (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ))
104	74	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ (∃x t = {{{x}}} ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
105		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃x(t = {{{x}}} ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ (∃x t = {{{x}}} ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
106	104, 105	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ ∃x(t = {{{x}}} ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
107	106	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ ∃t∃x(t = {{{x}}} ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
108		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
109		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃x∃t(t = {{{x}}} ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ ∃t∃x(t = {{{x}}} ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
110	107, 108, 109	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) ↔ ∃x∃t(t = {{{x}}} ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
111		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (t = {{{x}}} → ⟪t, ⟪n, {{b}}⟫⟫ = ⟪{{{x}}}, ⟪n, {{b}}⟫⟫)
112	111	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (t = {{{x}}} → (⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) ↔ ⟪{{{x}}}, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )))
113	82, 112	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃t(t = {{{x}}} ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ ⟪{{{x}}}, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ))
114		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟪{{{x}}}, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) ↔ (⟪{{{x}}}, ⟪n, {{b}}⟫⟫ ∈ Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∧ ⟪{{{x}}}, ⟪n, {{b}}⟫⟫ ∈ Ins3_k S_k ))
115	87, 69, 39	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟪{{{x}}}, ⟪n, {{b}}⟫⟫ ∈ Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ↔ ⟪{x}, {{b}}⟫ ∈ SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)))
116	89, 41	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟪{x}, {{b}}⟫ ∈ SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ↔ ⟪x, {b}⟫ ∈ ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)))
117	89, 43	eqpw1relk 4480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟪x, {b}⟫ ∈ ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ↔ x = ℘₁b)
118	115, 116, 117	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟪{{{x}}}, ⟪n, {{b}}⟫⟫ ∈ Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ↔ x = ℘₁b)
119	87, 69, 39	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟪{{{x}}}, ⟪n, {{b}}⟫⟫ ∈ Ins3_k S_k ↔ ⟪{x}, n⟫ ∈ S_k )
120	119, 94	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟪{{{x}}}, ⟪n, {{b}}⟫⟫ ∈ Ins3_k S_k ↔ x ∈ n)
121	118, 120	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟪{{{x}}}, ⟪n, {{b}}⟫⟫ ∈ Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∧ ⟪{{{x}}}, ⟪n, {{b}}⟫⟫ ∈ Ins3_k S_k ) ↔ (x = ℘₁b ∧ x ∈ n))
122	113, 114, 121	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃t(t = {{{x}}} ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ (x = ℘₁b ∧ x ∈ n))
123	122	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃x∃t(t = {{{x}}} ∧ ⟪t, ⟪n, {{b}}⟫⟫ ∈ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k )) ↔ ∃x(x = ℘₁b ∧ x ∈ n))
124	103, 110, 123	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟪n, {{b}}⟫ ∈ (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ↔ ∃x(x = ℘₁b ∧ x ∈ n))
125	69, 39, 12	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ↔ ⟪n, {{b}}⟫ ∈ (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))
126		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (℘₁b ∈ n ↔ ∃x(x = ℘₁b ∧ x ∈ n))
127	124, 125, 126	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ↔ ℘₁b ∈ n)
128	101, 127	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∧ ⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)) ↔ (℘₁a ∈ n ∧ ℘₁b ∈ n))
129	68, 128	bitri 240	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)) ↔ (℘₁a ∈ n ∧ ℘₁b ∈ n))
130	67, 129	anbi12i 678	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ (℘₁℘₁ Nn ×_k V) ∧ ⟪{{n}}, ⟪{{b}}, {{a}}⟫⟫ ∈ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) ↔ (n ∈ Nn ∧ (℘₁a ∈ n ∧ ℘₁b ∈ n)))
131	61, 62, 130	3bitri 262	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃t(t = {{n}} ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))) ↔ (n ∈ Nn ∧ (℘₁a ∈ n ∧ ℘₁b ∈ n)))
132	131	exbii 1582	. . . . . . . . . . . . . . . . . 18 ⊢ (∃n∃t(t = {{n}} ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))) ↔ ∃n(n ∈ Nn ∧ (℘₁a ∈ n ∧ ℘₁b ∈ n)))
133		df-rex 2621	. . . . . . . . . . . . . . . . . 18 ⊢ (∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n) ↔ ∃n(n ∈ Nn ∧ (℘₁a ∈ n ∧ ℘₁b ∈ n)))
134	132, 133	bitr4i 243	. . . . . . . . . . . . . . . . 17 ⊢ (∃n∃t(t = {{n}} ∧ ⟪t, ⟪{{b}}, {{a}}⟫⟫ ∈ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)))) ↔ ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n))
135	46, 57, 134	3bitri 262	. . . . . . . . . . . . . . . 16 ⊢ (⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ∈ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c) ↔ ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n))
136	135	notbii 287	. . . . . . . . . . . . . . 15 ⊢ (¬ ⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ∈ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c) ↔ ¬ ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n))
137	45, 136	anbi12i 678	. . . . . . . . . . . . . 14 ⊢ ((⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ∈ Ins2_k SI_k S_k ∧ ¬ ⟪{{{{b}}}}, ⟪{{a}}, {m}⟫⟫ ∈ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) ↔ (b ∈ m ∧ ¬ ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n)))
138	37, 38, 137	3bitri 262	. . . . . . . . . . . . 13 ⊢ (∃t(t = {{{{b}}}} ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))) ↔ (b ∈ m ∧ ¬ ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n)))
139	138	exbii 1582	. . . . . . . . . . . 12 ⊢ (∃b∃t(t = {{{{b}}}} ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))) ↔ ∃b(b ∈ m ∧ ¬ ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n)))
140		df-rex 2621	. . . . . . . . . . . 12 ⊢ (∃b ∈ m ¬ ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n) ↔ ∃b(b ∈ m ∧ ¬ ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n)))
141	139, 140	bitr4i 243	. . . . . . . . . . 11 ⊢ (∃b∃t(t = {{{{b}}}} ∧ ⟪t, ⟪{{a}}, {m}⟫⟫ ∈ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c))) ↔ ∃b ∈ m ¬ ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n))
142		rexnal 2626	. . . . . . . . . . 11 ⊢ (∃b ∈ m ¬ ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n) ↔ ¬ ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n))
143	33, 141, 142	3bitri 262	. . . . . . . . . 10 ⊢ (⟪{{a}}, {m}⟫ ∈ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c) ↔ ¬ ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n))
144	22, 143	anbi12i 678	. . . . . . . . 9 ⊢ ((⟪{{a}}, {m}⟫ ∈ SI_k S_k ∧ ⟪{{a}}, {m}⟫ ∈ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ↔ (a ∈ m ∧ ¬ ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n)))
145	15, 16, 144	3bitri 262	. . . . . . . 8 ⊢ (∃t(t = {{a}} ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))) ↔ (a ∈ m ∧ ¬ ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n)))
146	145	exbii 1582	. . . . . . 7 ⊢ (∃a∃t(t = {{a}} ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))) ↔ ∃a(a ∈ m ∧ ¬ ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n)))
147		df-rex 2621	. . . . . . 7 ⊢ (∃a ∈ m ¬ ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n) ↔ ∃a(a ∈ m ∧ ¬ ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n)))
148	146, 147	bitr4i 243	. . . . . 6 ⊢ (∃a∃t(t = {{a}} ∧ ⟪t, {m}⟫ ∈ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c))) ↔ ∃a ∈ m ¬ ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n))
149	3, 11, 148	3bitri 262	. . . . 5 ⊢ ({m} ∈ (( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) “_k ℘₁1_c) ↔ ∃a ∈ m ¬ ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n))
150	2, 149	xchbinx 301	. . . 4 ⊢ ({m} ∈ ∼ (( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) “_k ℘₁1_c) ↔ ¬ ∃a ∈ m ¬ ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n))
151	18	eluni1 4174	. . . 4 ⊢ (m ∈ ⋃₁ ∼ (( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) “_k ℘₁1_c) ↔ {m} ∈ ∼ (( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) “_k ℘₁1_c))
152		dfral2 2627	. . . 4 ⊢ (∀a ∈ m ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n) ↔ ¬ ∃a ∈ m ¬ ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n))
153	150, 151, 152	3bitr4i 268	. . 3 ⊢ (m ∈ ⋃₁ ∼ (( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) “_k ℘₁1_c) ↔ ∀a ∈ m ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n))
154	153	eqabi 2465	. 2 ⊢ ⋃₁ ∼ (( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) “_k ℘₁1_c) = {m ∣ ∀a ∈ m ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n)}
155		ssetkex 4295	. . . . . . 7 ⊢ S_k ∈ V
156	155	sikex 4298	. . . . . 6 ⊢ SI_k S_k ∈ V
157	156	ins2kex 4308	. . . . . . . 8 ⊢ Ins2_k SI_k S_k ∈ V
158		nncex 4397	. . . . . . . . . . . . . 14 ⊢ Nn ∈ V
159	158	pw1ex 4304	. . . . . . . . . . . . 13 ⊢ ℘₁ Nn ∈ V
160	159	pw1ex 4304	. . . . . . . . . . . 12 ⊢ ℘₁℘₁ Nn ∈ V
161		vvex 4110	. . . . . . . . . . . 12 ⊢ V ∈ V
162	160, 161	xpkex 4290	. . . . . . . . . . 11 ⊢ (℘₁℘₁ Nn ×_k V) ∈ V
163		1cex 4143	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1_c ∈ V
164	163	pwex 4330	. . . . . . . . . . . . . . . . . . 19 ⊢ ℘1_c ∈ V
165	164, 161	xpkex 4290	. . . . . . . . . . . . . . . . . 18 ⊢ (℘1_c ×_k V) ∈ V
166	155	ins3kex 4309	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ins3_k S_k ∈ V
167	166, 157	symdifex 4109	. . . . . . . . . . . . . . . . . . 19 ⊢ ( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) ∈ V
168	163	pw1ex 4304	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℘₁1_c ∈ V
169	168	pw1ex 4304	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℘₁℘₁1_c ∈ V
170	169	pw1ex 4304	. . . . . . . . . . . . . . . . . . 19 ⊢ ℘₁℘₁℘₁1_c ∈ V
171	167, 170	imakex 4301	. . . . . . . . . . . . . . . . . 18 ⊢ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c) ∈ V
172	165, 171	difex 4108	. . . . . . . . . . . . . . . . 17 ⊢ ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∈ V
173	172	sikex 4298	. . . . . . . . . . . . . . . 16 ⊢ SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∈ V
174	173	ins2kex 4308	. . . . . . . . . . . . . . 15 ⊢ Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∈ V
175	174, 166	inex 4106	. . . . . . . . . . . . . 14 ⊢ ( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) ∈ V
176	175, 169	imakex 4301	. . . . . . . . . . . . 13 ⊢ (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∈ V
177	176	ins2kex 4308	. . . . . . . . . . . 12 ⊢ Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∈ V
178	176	ins3kex 4309	. . . . . . . . . . . 12 ⊢ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∈ V
179	177, 178	inex 4106	. . . . . . . . . . 11 ⊢ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c)) ∈ V
180	162, 179	inex 4106	. . . . . . . . . 10 ⊢ ((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) ∈ V
181	180, 168	imakex 4301	. . . . . . . . 9 ⊢ (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c) ∈ V
182	181	ins3kex 4309	. . . . . . . 8 ⊢ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c) ∈ V
183	157, 182	difex 4108	. . . . . . 7 ⊢ ( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) ∈ V
184	183, 170	imakex 4301	. . . . . 6 ⊢ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c) ∈ V
185	156, 184	inex 4106	. . . . 5 ⊢ ( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) ∈ V
186	185, 168	imakex 4301	. . . 4 ⊢ (( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) “_k ℘₁1_c) ∈ V
187	186	complex 4105	. . 3 ⊢ ∼ (( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) “_k ℘₁1_c) ∈ V
188	187	uni1ex 4294	. 2 ⊢ ⋃₁ ∼ (( SI_k S_k ∩ (( Ins2_k SI_k S_k ∖ Ins3_k (((℘₁℘₁ Nn ×_k V) ∩ ( Ins2_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c) ∩ Ins3_k (( Ins2_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∩ Ins3_k S_k ) “_k ℘₁℘₁1_c))) “_k ℘₁1_c)) “_k ℘₁℘₁℘₁1_c)) “_k ℘₁1_c) ∈ V
189	154, 188	eqeltrri 2424	1 ⊢ {m ∣ ∀a ∈ m ∀b ∈ m ∃n ∈ Nn (℘₁a ∈ n ∧ ℘₁b ∈ n)} ∈ V

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ∧ wa 358 ∃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 ⟪copk 4058 ⋃₁cuni1 4134 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

This theorem was proved from 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 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 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

This theorem is referenced by: ncfinraise 4482

W3C validator