eqtfinrelk - New Foundations Explorer

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

Theorem eqtfinrelk 4486

Description: Equality to a T raising expressed via a Kuratowski relationship. (Contributed by SF, 29-Jan-2015.)

**Hypotheses**
Ref	Expression
eqtfinrelk.1	⊢ M ∈ V
eqtfinrelk.2	⊢ X ∈ V

**Assertion**
Ref	Expression
eqtfinrelk	⊢ (⟪{M}, X⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ X = T_fin M)

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

Step	Hyp	Ref	Expression
1		snex 4111	. . . . . . . . . 10 ⊢ {∅} ∈ V
2	1	snid 3760	. . . . . . . . 9 ⊢ {∅} ∈ {{∅}}
3		eqtfinrelk.2	. . . . . . . . . 10 ⊢ X ∈ V
4	1, 3	opkelxpk 4248	. . . . . . . . 9 ⊢ (⟪{∅}, X⟫ ∈ ({{∅}} ×_k {∅}) ↔ ({∅} ∈ {{∅}} ∧ X ∈ {∅}))
5	2, 4	mpbiran 884	. . . . . . . 8 ⊢ (⟪{∅}, X⟫ ∈ ({{∅}} ×_k {∅}) ↔ X ∈ {∅})
6	3	elsnc 3756	. . . . . . . 8 ⊢ (X ∈ {∅} ↔ X = ∅)
7	5, 6	bitri 240	. . . . . . 7 ⊢ (⟪{∅}, X⟫ ∈ ({{∅}} ×_k {∅}) ↔ X = ∅)
8	7	orbi1i 506	. . . . . 6 ⊢ ((⟪{∅}, X⟫ ∈ ({{∅}} ×_k {∅}) ∨ ⟪{∅}, X⟫ ∈ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ (X = ∅ ∨ ⟪{∅}, X⟫ ∈ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))))
9		elun 3220	. . . . . 6 ⊢ (⟪{∅}, X⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ (⟪{∅}, X⟫ ∈ ({{∅}} ×_k {∅}) ∨ ⟪{∅}, X⟫ ∈ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))))
10	1, 3	opkelxpk 4248	. . . . . . . . . . 11 ⊢ (⟪{∅}, X⟫ ∈ ({{∅}} ×_k V) ↔ ({∅} ∈ {{∅}} ∧ X ∈ V))
11	2, 3, 10	mpbir2an 886	. . . . . . . . . 10 ⊢ ⟪{∅}, X⟫ ∈ ({{∅}} ×_k V)
12	11	notnoti 115	. . . . . . . . 9 ⊢ ¬ ¬ ⟪{∅}, X⟫ ∈ ({{∅}} ×_k V)
13	12	intnan 880	. . . . . . . 8 ⊢ ¬ (⟪{∅}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∧ ¬ ⟪{∅}, X⟫ ∈ ({{∅}} ×_k V))
14		eldif 3221	. . . . . . . 8 ⊢ (⟪{∅}, X⟫ ∈ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)) ↔ (⟪{∅}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∧ ¬ ⟪{∅}, X⟫ ∈ ({{∅}} ×_k V)))
15	13, 14	mtbir 290	. . . . . . 7 ⊢ ¬ ⟪{∅}, X⟫ ∈ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))
16	15	biorfi 396	. . . . . 6 ⊢ (X = ∅ ↔ (X = ∅ ∨ ⟪{∅}, X⟫ ∈ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))))
17	8, 9, 16	3bitr4i 268	. . . . 5 ⊢ (⟪{∅}, X⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ X = ∅)
18	17	a1i 10	. . . 4 ⊢ (M = ∅ → (⟪{∅}, X⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ X = ∅))
19		sneq 3744	. . . . . 6 ⊢ (M = ∅ → {M} = {∅})
20	19	opkeq1d 4065	. . . . 5 ⊢ (M = ∅ → ⟪{M}, X⟫ = ⟪{∅}, X⟫)
21	20	eleq1d 2419	. . . 4 ⊢ (M = ∅ → (⟪{M}, X⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ ⟪{∅}, X⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
22		iftrue 3668	. . . . 5 ⊢ (M = ∅ → if(M = ∅, ∅, (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))) = ∅)
23	22	eqeq2d 2364	. . . 4 ⊢ (M = ∅ → (X = if(M = ∅, ∅, (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))) ↔ X = ∅))
24	18, 21, 23	3bitr4d 276	. . 3 ⊢ (M = ∅ → (⟪{M}, X⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ X = if(M = ∅, ∅, (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y)))))
25		iffalse 3669	. . . . 5 ⊢ (¬ M = ∅ → if(M = ∅, ∅, (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))) = (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y)))
26	25	eqeq2d 2364	. . . 4 ⊢ (¬ M = ∅ → (X = if(M = ∅, ∅, (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))) ↔ X = (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))))
27		opkex 4113	. . . . . . . . 9 ⊢ ⟪{M}, X⟫ ∈ V
28	27	elimak 4259	. . . . . . . 8 ⊢ (⟪{M}, X⟫ ∈ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)))
29		elpw121c 4148	. . . . . . . . . . . 12 ⊢ (t ∈ ℘₁℘₁1_c ↔ ∃z t = {{{z}}})
30	29	anbi1i 676	. . . . . . . . . . 11 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))) ↔ (∃z t = {{{z}}} ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))))
31		19.41v 1901	. . . . . . . . . . 11 ⊢ (∃z(t = {{{z}}} ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))) ↔ (∃z t = {{{z}}} ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))))
32	30, 31	bitr4i 243	. . . . . . . . . 10 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))) ↔ ∃z(t = {{{z}}} ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))))
33	32	exbii 1582	. . . . . . . . 9 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))) ↔ ∃t∃z(t = {{{z}}} ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))))
34		df-rex 2620	. . . . . . . . 9 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))))
35		excom 1741	. . . . . . . . 9 ⊢ (∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))) ↔ ∃t∃z(t = {{{z}}} ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))))
36	33, 34, 35	3bitr4i 268	. . . . . . . 8 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) ↔ ∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))))
37		snex 4111	. . . . . . . . . . 11 ⊢ {{{z}}} ∈ V
38		opkeq1 4059	. . . . . . . . . . . 12 ⊢ (t = {{{z}}} → ⟪t, ⟪{M}, X⟫⟫ = ⟪{{{z}}}, ⟪{M}, X⟫⟫)
39	38	eleq1d 2419	. . . . . . . . . . 11 ⊢ (t = {{{z}}} → (⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) ↔ ⟪{{{z}}}, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))))
40	37, 39	ceqsexv 2894	. . . . . . . . . 10 ⊢ (∃t(t = {{{z}}} ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))) ↔ ⟪{{{z}}}, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)))
41		elsymdif 3223	. . . . . . . . . . 11 ⊢ (⟪{{{z}}}, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) ↔ ¬ (⟪{{{z}}}, ⟪{M}, X⟫⟫ ∈ Ins2_k S_k ↔ ⟪{{{z}}}, ⟪{M}, X⟫⟫ ∈ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)))
42		snex 4111	. . . . . . . . . . . . . 14 ⊢ {z} ∈ V
43		snex 4111	. . . . . . . . . . . . . 14 ⊢ {M} ∈ V
44	42, 43, 3	otkelins2k 4255	. . . . . . . . . . . . 13 ⊢ (⟪{{{z}}}, ⟪{M}, X⟫⟫ ∈ Ins2_k S_k ↔ ⟪{z}, X⟫ ∈ S_k )
45		vex 2862	. . . . . . . . . . . . . 14 ⊢ z ∈ V
46	45, 3	elssetk 4270	. . . . . . . . . . . . 13 ⊢ (⟪{z}, X⟫ ∈ S_k ↔ z ∈ X)
47	44, 46	bitri 240	. . . . . . . . . . . 12 ⊢ (⟪{{{z}}}, ⟪{M}, X⟫⟫ ∈ Ins2_k S_k ↔ z ∈ X)
48		snex 4111	. . . . . . . . . . . . . . . 16 ⊢ {{n}} ∈ V
49		opkeq1 4059	. . . . . . . . . . . . . . . . 17 ⊢ (t = {{n}} → ⟪t, ⟪{z}, {M}⟫⟫ = ⟪{{n}}, ⟪{z}, {M}⟫⟫)
50	49	eleq1d 2419	. . . . . . . . . . . . . . . 16 ⊢ (t = {{n}} → (⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) ↔ ⟪{{n}}, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))))
51	48, 50	ceqsexv 2894	. . . . . . . . . . . . . . 15 ⊢ (∃t(t = {{n}} ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))) ↔ ⟪{{n}}, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)))
52		eldif 3221	. . . . . . . . . . . . . . 15 ⊢ (⟪{{n}}, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) ↔ (⟪{{n}}, ⟪{z}, {M}⟫⟫ ∈ Ins3_k ^◡_k S_k ∧ ¬ ⟪{{n}}, ⟪{z}, {M}⟫⟫ ∈ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)))
53		vex 2862	. . . . . . . . . . . . . . . . . 18 ⊢ n ∈ V
54	53, 42, 43	otkelins3k 4256	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{{n}}, ⟪{z}, {M}⟫⟫ ∈ Ins3_k ^◡_k S_k ↔ ⟪n, {z}⟫ ∈ ^◡_k S_k )
55	53, 42	opkelcnvk 4250	. . . . . . . . . . . . . . . . 17 ⊢ (⟪n, {z}⟫ ∈ ^◡_k S_k ↔ ⟪{z}, n⟫ ∈ S_k )
56	45, 53	elssetk 4270	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{z}, n⟫ ∈ S_k ↔ z ∈ n)
57	54, 55, 56	3bitri 262	. . . . . . . . . . . . . . . 16 ⊢ (⟪{{n}}, ⟪{z}, {M}⟫⟫ ∈ Ins3_k ^◡_k S_k ↔ z ∈ n)
58	53, 42, 43	otkelins2k 4255	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪{{n}}, ⟪{z}, {M}⟫⟫ ∈ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c) ↔ ⟪n, {M}⟫ ∈ (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))
59		opkex 4113	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟪n, {M}⟫ ∈ V
60	59	elimak 4259	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪n, {M}⟫ ∈ (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c) ↔ ∃t ∈ ℘₁ 1_c⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ))
61		elpw11c 4147	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (t ∈ ℘₁1_c ↔ ∃y t = {{y}})
62	61	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((t ∈ ℘₁1_c ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )) ↔ (∃y t = {{y}} ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )))
63		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃y(t = {{y}} ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )) ↔ (∃y t = {{y}} ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )))
64	62, 63	bitr4i 243	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((t ∈ ℘₁1_c ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )) ↔ ∃y(t = {{y}} ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )))
65	64	exbii 1582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃t(t ∈ ℘₁1_c ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )) ↔ ∃t∃y(t = {{y}} ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )))
66		df-rex 2620	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃t ∈ ℘₁ 1_c⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) ↔ ∃t(t ∈ ℘₁1_c ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )))
67		excom 1741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃y∃t(t = {{y}} ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )) ↔ ∃t∃y(t = {{y}} ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )))
68	65, 66, 67	3bitr4i 268	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃t ∈ ℘₁ 1_c⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) ↔ ∃y∃t(t = {{y}} ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )))
69		snex 4111	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {{y}} ∈ V
70		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (t = {{y}} → ⟪t, ⟪n, {M}⟫⟫ = ⟪{{y}}, ⟪n, {M}⟫⟫)
71	70	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (t = {{y}} → (⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) ↔ ⟪{{y}}, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )))
72	69, 71	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃t(t = {{y}} ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )) ↔ ⟪{{y}}, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ))
73		elsymdif 3223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟪{{y}}, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) ↔ ¬ (⟪{{y}}, ⟪n, {M}⟫⟫ ∈ Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ↔ ⟪{{y}}, ⟪n, {M}⟫⟫ ∈ Ins3_k I_k ))
74		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ y ∈ V
75	74, 53, 43	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟪{{y}}, ⟪n, {M}⟫⟫ ∈ Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ↔ ⟪y, {M}⟫ ∈ (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)))
76		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟪y, {M}⟫ ∈ (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ↔ (⟪y, {M}⟫ ∈ ( Nn ×_k V) ∧ ⟪y, {M}⟫ ∈ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)))
77	74, 43	opkelxpk 4248	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪y, {M}⟫ ∈ ( Nn ×_k V) ↔ (y ∈ Nn ∧ {M} ∈ V))
78	43, 77	mpbiran2 885	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟪y, {M}⟫ ∈ ( Nn ×_k V) ↔ y ∈ Nn )
79		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ {{{{a}}}} ∈ V
80		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (t = {{{{a}}}} → ⟪t, ⟪y, {M}⟫⟫ = ⟪{{{{a}}}}, ⟪y, {M}⟫⟫)
81	80	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (t = {{{{a}}}} → (⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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)) ↔ ⟪{{{{a}}}}, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))))
82	79, 81	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃t(t = {{{{a}}}} ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))) ↔ ⟪{{{{a}}}}, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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)))
83		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟪{{{{a}}}}, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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)) ↔ (⟪{{{{a}}}}, ⟪y, {M}⟫⟫ ∈ Ins2_k SI_k S_k ∧ ⟪{{{{a}}}}, ⟪y, {M}⟫⟫ ∈ 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)))
84		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ {{a}} ∈ V
85	84, 74, 43	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟪{{{{a}}}}, ⟪y, {M}⟫⟫ ∈ Ins2_k SI_k S_k ↔ ⟪{{a}}, {M}⟫ ∈ SI_k S_k )
86		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ {a} ∈ V
87		eqtfinrelk.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ M ∈ V
88	86, 87	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟪{{a}}, {M}⟫ ∈ SI_k S_k ↔ ⟪{a}, M⟫ ∈ S_k )
89		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ a ∈ V
90	89, 87	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟪{a}, M⟫ ∈ S_k ↔ a ∈ M)
91	85, 88, 90	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟪{{{{a}}}}, ⟪y, {M}⟫⟫ ∈ Ins2_k SI_k S_k ↔ a ∈ M)
92		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ⟪{{a}}, y⟫ ∈ V
93	92	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟪{{a}}, y⟫ ∈ (( 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) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 ))
94		elpw121c 4148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (t ∈ ℘₁℘₁1_c ↔ ∃x t = {{{x}}})
95	94	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )) ↔ (∃x t = {{{x}}} ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )))
96		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃x(t = {{{x}}} ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )) ↔ (∃x t = {{{x}}} ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )))
97	95, 96	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )) ↔ ∃x(t = {{{x}}} ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )))
98	97	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )) ↔ ∃t∃x(t = {{{x}}} ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )))
99		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 ) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )))
100		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∃x∃t(t = {{{x}}} ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )) ↔ ∃t∃x(t = {{{x}}} ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )))
101	98, 99, 100	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 ) ↔ ∃x∃t(t = {{{x}}} ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )))
102		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {{{x}}} ∈ V
103		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (t = {{{x}}} → ⟪t, ⟪{{a}}, y⟫⟫ = ⟪{{{x}}}, ⟪{{a}}, y⟫⟫)
104	103	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (t = {{{x}}} → (⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 ) ↔ ⟪{{{x}}}, ⟪{{a}}, y⟫⟫ ∈ ( 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 )))
105	102, 104	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∃t(t = {{{x}}} ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )) ↔ ⟪{{{x}}}, ⟪{{a}}, y⟫⟫ ∈ ( 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 ))
106		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟪{{{x}}}, ⟪{{a}}, y⟫⟫ ∈ ( 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 ) ↔ (⟪{{{x}}}, ⟪{{a}}, y⟫⟫ ∈ Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∧ ⟪{{{x}}}, ⟪{{a}}, y⟫⟫ ∈ Ins2_k S_k ))
107		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ {x} ∈ V
108	107, 84, 74	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟪{{{x}}}, ⟪{{a}}, y⟫⟫ ∈ Ins3_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)))
109		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ x ∈ V
110	109, 86	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟪{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)))
111	109, 89	eqpw1relk 4479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟪x, {a}⟫ ∈ ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ↔ x = ℘₁a)
112	108, 110, 111	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟪{{{x}}}, ⟪{{a}}, y⟫⟫ ∈ Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ↔ x = ℘₁a)
113	107, 84, 74	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟪{{{x}}}, ⟪{{a}}, y⟫⟫ ∈ Ins2_k S_k ↔ ⟪{x}, y⟫ ∈ S_k )
114	109, 74	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟪{x}, y⟫ ∈ S_k ↔ x ∈ y)
115	113, 114	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟪{{{x}}}, ⟪{{a}}, y⟫⟫ ∈ Ins2_k S_k ↔ x ∈ y)
116	112, 115	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((⟪{{{x}}}, ⟪{{a}}, y⟫⟫ ∈ Ins3_k SI_k ((℘1_c ×_k V) ∖ (( Ins3_k S_k ⊕ Ins2_k SI_k S_k ) “_k ℘₁℘₁℘₁1_c)) ∧ ⟪{{{x}}}, ⟪{{a}}, y⟫⟫ ∈ Ins2_k S_k ) ↔ (x = ℘₁a ∧ x ∈ y))
117	105, 106, 116	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∃t(t = {{{x}}} ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )) ↔ (x = ℘₁a ∧ x ∈ y))
118	117	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃x∃t(t = {{{x}}} ∧ ⟪t, ⟪{{a}}, y⟫⟫ ∈ ( 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 )) ↔ ∃x(x = ℘₁a ∧ x ∈ y))
119	93, 101, 118	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟪{{a}}, y⟫ ∈ (( 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) ↔ ∃x(x = ℘₁a ∧ x ∈ y))
120	84, 74, 43	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟪{{{{a}}}}, ⟪y, {M}⟫⟫ ∈ 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) ↔ ⟪{{a}}, y⟫ ∈ (( 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))
121		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (℘₁a ∈ y ↔ ∃x(x = ℘₁a ∧ x ∈ y))
122	119, 120, 121	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟪{{{{a}}}}, ⟪y, {M}⟫⟫ ∈ 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) ↔ ℘₁a ∈ y)
123	91, 122	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((⟪{{{{a}}}}, ⟪y, {M}⟫⟫ ∈ Ins2_k SI_k S_k ∧ ⟪{{{{a}}}}, ⟪y, {M}⟫⟫ ∈ 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)) ↔ (a ∈ M ∧ ℘₁a ∈ y))
124	82, 83, 123	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃t(t = {{{{a}}}} ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))) ↔ (a ∈ M ∧ ℘₁a ∈ y))
125	124	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃a∃t(t = {{{{a}}}} ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))) ↔ ∃a(a ∈ M ∧ ℘₁a ∈ y))
126		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃t ∈ ℘₁ ℘₁℘₁1_c⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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)) ↔ ∃t(t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))))
127		elpw131c 4149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (t ∈ ℘₁℘₁℘₁1_c ↔ ∃a t = {{{{a}}}})
128	127	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))) ↔ (∃a t = {{{{a}}}} ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))))
129		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∃a(t = {{{{a}}}} ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))) ↔ (∃a t = {{{{a}}}} ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))))
130	128, 129	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))) ↔ ∃a(t = {{{{a}}}} ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))))
131	130	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃t(t ∈ ℘₁℘₁℘₁1_c ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))) ↔ ∃t∃a(t = {{{{a}}}} ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))))
132	126, 131	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃t ∈ ℘₁ ℘₁℘₁1_c⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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)) ↔ ∃t∃a(t = {{{{a}}}} ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))))
133		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ⟪y, {M}⟫ ∈ V
134	133	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟪y, {M}⟫ ∈ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁℘₁1_c⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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)))
135		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃a∃t(t = {{{{a}}}} ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))) ↔ ∃t∃a(t = {{{{a}}}} ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))))
136	132, 134, 135	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪y, {M}⟫ ∈ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c) ↔ ∃a∃t(t = {{{{a}}}} ∧ ⟪t, ⟪y, {M}⟫⟫ ∈ ( Ins2_k SI_k S_k ∩ 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))))
137		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃a ∈ M ℘₁a ∈ y ↔ ∃a(a ∈ M ∧ ℘₁a ∈ y))
138	125, 136, 137	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟪y, {M}⟫ ∈ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c) ↔ ∃a ∈ M ℘₁a ∈ y)
139	78, 138	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((⟪y, {M}⟫ ∈ ( Nn ×_k V) ∧ ⟪y, {M}⟫ ∈ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ↔ (y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))
140	75, 76, 139	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪{{y}}, ⟪n, {M}⟫⟫ ∈ Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ↔ (y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))
141	74, 53, 43	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟪{{y}}, ⟪n, {M}⟫⟫ ∈ Ins3_k I_k ↔ ⟪y, n⟫ ∈ I_k )
142		opkelidkg 4274	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((y ∈ V ∧ n ∈ V) → (⟪y, n⟫ ∈ I_k ↔ y = n))
143	74, 53, 142	mp2an 653	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟪y, n⟫ ∈ I_k ↔ y = n)
144	141, 143	bitri 240	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪{{y}}, ⟪n, {M}⟫⟫ ∈ Ins3_k I_k ↔ y = n)
145	140, 144	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⟪{{y}}, ⟪n, {M}⟫⟫ ∈ Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ↔ ⟪{{y}}, ⟪n, {M}⟫⟫ ∈ Ins3_k I_k ) ↔ ((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n))
146	73, 145	xchbinx 301	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟪{{y}}, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) ↔ ¬ ((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n))
147	72, 146	bitri 240	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃t(t = {{y}} ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )) ↔ ¬ ((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n))
148	147	exbii 1582	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃y∃t(t = {{y}} ∧ ⟪t, ⟪n, {M}⟫⟫ ∈ ( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k )) ↔ ∃y ¬ ((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n))
149	60, 68, 148	3bitri 262	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪n, {M}⟫ ∈ (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c) ↔ ∃y ¬ ((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n))
150		exnal 1574	. . . . . . . . . . . . . . . . . 18 ⊢ (∃y ¬ ((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n) ↔ ¬ ∀y((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n))
151	58, 149, 150	3bitrri 263	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ∀y((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n) ↔ ⟪{{n}}, ⟪{z}, {M}⟫⟫ ∈ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))
152	151	con1bii 321	. . . . . . . . . . . . . . . 16 ⊢ (¬ ⟪{{n}}, ⟪{z}, {M}⟫⟫ ∈ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c) ↔ ∀y((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n))
153	57, 152	anbi12i 678	. . . . . . . . . . . . . . 15 ⊢ ((⟪{{n}}, ⟪{z}, {M}⟫⟫ ∈ Ins3_k ^◡_k S_k ∧ ¬ ⟪{{n}}, ⟪{z}, {M}⟫⟫ ∈ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) ↔ (z ∈ n ∧ ∀y((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n)))
154	51, 52, 153	3bitri 262	. . . . . . . . . . . . . 14 ⊢ (∃t(t = {{n}} ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))) ↔ (z ∈ n ∧ ∀y((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n)))
155	154	exbii 1582	. . . . . . . . . . . . 13 ⊢ (∃n∃t(t = {{n}} ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))) ↔ ∃n(z ∈ n ∧ ∀y((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n)))
156	42, 43, 3	otkelins3k 4256	. . . . . . . . . . . . . 14 ⊢ (⟪{{{z}}}, ⟪{M}, X⟫⟫ ∈ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c) ↔ ⟪{z}, {M}⟫ ∈ (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))
157		opkex 4113	. . . . . . . . . . . . . . 15 ⊢ ⟪{z}, {M}⟫ ∈ V
158	157	elimak 4259	. . . . . . . . . . . . . 14 ⊢ (⟪{z}, {M}⟫ ∈ (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c) ↔ ∃t ∈ ℘₁ 1_c⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)))
159		elpw11c 4147	. . . . . . . . . . . . . . . . . 18 ⊢ (t ∈ ℘₁1_c ↔ ∃n t = {{n}})
160	159	anbi1i 676	. . . . . . . . . . . . . . . . 17 ⊢ ((t ∈ ℘₁1_c ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))) ↔ (∃n t = {{n}} ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))))
161		19.41v 1901	. . . . . . . . . . . . . . . . 17 ⊢ (∃n(t = {{n}} ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))) ↔ (∃n t = {{n}} ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))))
162	160, 161	bitr4i 243	. . . . . . . . . . . . . . . 16 ⊢ ((t ∈ ℘₁1_c ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))) ↔ ∃n(t = {{n}} ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))))
163	162	exbii 1582	. . . . . . . . . . . . . . 15 ⊢ (∃t(t ∈ ℘₁1_c ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))) ↔ ∃t∃n(t = {{n}} ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))))
164		df-rex 2620	. . . . . . . . . . . . . . 15 ⊢ (∃t ∈ ℘₁ 1_c⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) ↔ ∃t(t ∈ ℘₁1_c ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))))
165		excom 1741	. . . . . . . . . . . . . . 15 ⊢ (∃n∃t(t = {{n}} ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))) ↔ ∃t∃n(t = {{n}} ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))))
166	163, 164, 165	3bitr4i 268	. . . . . . . . . . . . . 14 ⊢ (∃t ∈ ℘₁ 1_c⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) ↔ ∃n∃t(t = {{n}} ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))))
167	156, 158, 166	3bitri 262	. . . . . . . . . . . . 13 ⊢ (⟪{{{z}}}, ⟪{M}, X⟫⟫ ∈ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c) ↔ ∃n∃t(t = {{n}} ∧ ⟪t, ⟪{z}, {M}⟫⟫ ∈ ( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c))))
168		dfiota2 4340	. . . . . . . . . . . . . . 15 ⊢ (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y)) = ∪{n ∣ ∀y((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n)}
169	168	eleq2i 2417	. . . . . . . . . . . . . 14 ⊢ (z ∈ (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y)) ↔ z ∈ ∪{n ∣ ∀y((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n)})
170		eluniab 3903	. . . . . . . . . . . . . 14 ⊢ (z ∈ ∪{n ∣ ∀y((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n)} ↔ ∃n(z ∈ n ∧ ∀y((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n)))
171	169, 170	bitri 240	. . . . . . . . . . . . 13 ⊢ (z ∈ (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y)) ↔ ∃n(z ∈ n ∧ ∀y((y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y) ↔ y = n)))
172	155, 167, 171	3bitr4i 268	. . . . . . . . . . . 12 ⊢ (⟪{{{z}}}, ⟪{M}, X⟫⟫ ∈ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c) ↔ z ∈ (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y)))
173	47, 172	bibi12i 306	. . . . . . . . . . 11 ⊢ ((⟪{{{z}}}, ⟪{M}, X⟫⟫ ∈ Ins2_k S_k ↔ ⟪{{{z}}}, ⟪{M}, X⟫⟫ ∈ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) ↔ (z ∈ X ↔ z ∈ (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))))
174	41, 173	xchbinx 301	. . . . . . . . . 10 ⊢ (⟪{{{z}}}, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) ↔ ¬ (z ∈ X ↔ z ∈ (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))))
175	40, 174	bitri 240	. . . . . . . . 9 ⊢ (∃t(t = {{{z}}} ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))) ↔ ¬ (z ∈ X ↔ z ∈ (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))))
176	175	exbii 1582	. . . . . . . 8 ⊢ (∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪{M}, X⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c))) ↔ ∃z ¬ (z ∈ X ↔ z ∈ (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))))
177	28, 36, 176	3bitri 262	. . . . . . 7 ⊢ (⟪{M}, X⟫ ∈ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ∃z ¬ (z ∈ X ↔ z ∈ (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))))
178	177	notbii 287	. . . . . 6 ⊢ (¬ ⟪{M}, X⟫ ∈ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ¬ ∃z ¬ (z ∈ X ↔ z ∈ (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))))
179	27	elcompl 3225	. . . . . 6 ⊢ (⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ¬ ⟪{M}, X⟫ ∈ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c))
180		dfcleq 2347	. . . . . . 7 ⊢ (X = (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y)) ↔ ∀z(z ∈ X ↔ z ∈ (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))))
181		alex 1572	. . . . . . 7 ⊢ (∀z(z ∈ X ↔ z ∈ (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))) ↔ ¬ ∃z ¬ (z ∈ X ↔ z ∈ (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))))
182	180, 181	bitri 240	. . . . . 6 ⊢ (X = (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y)) ↔ ¬ ∃z ¬ (z ∈ X ↔ z ∈ (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))))
183	178, 179, 182	3bitr4i 268	. . . . 5 ⊢ (⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ↔ X = (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y)))
184	183	a1i 10	. . . 4 ⊢ (¬ M = ∅ → (⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ↔ X = (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))))
185	43, 3	opkelxpk 4248	. . . . . . . . . . 11 ⊢ (⟪{M}, X⟫ ∈ ({{∅}} ×_k V) ↔ ({M} ∈ {{∅}} ∧ X ∈ V))
186	3	biantru 491	. . . . . . . . . . 11 ⊢ ({M} ∈ {{∅}} ↔ ({M} ∈ {{∅}} ∧ X ∈ V))
187	43	elsnc 3756	. . . . . . . . . . . 12 ⊢ ({M} ∈ {{∅}} ↔ {M} = {∅})
188	87	sneqb 3876	. . . . . . . . . . . 12 ⊢ ({M} = {∅} ↔ M = ∅)
189	187, 188	bitri 240	. . . . . . . . . . 11 ⊢ ({M} ∈ {{∅}} ↔ M = ∅)
190	185, 186, 189	3bitr2i 264	. . . . . . . . . 10 ⊢ (⟪{M}, X⟫ ∈ ({{∅}} ×_k V) ↔ M = ∅)
191	190	biimpi 186	. . . . . . . . 9 ⊢ (⟪{M}, X⟫ ∈ ({{∅}} ×_k V) → M = ∅)
192	191	con3i 127	. . . . . . . 8 ⊢ (¬ M = ∅ → ¬ ⟪{M}, X⟫ ∈ ({{∅}} ×_k V))
193	192	biantrud 493	. . . . . . 7 ⊢ (¬ M = ∅ → (⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ↔ (⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∧ ¬ ⟪{M}, X⟫ ∈ ({{∅}} ×_k V))))
194		simpl 443	. . . . . . . . 9 ⊢ ((M = ∅ ∧ X = ∅) → M = ∅)
195	194	con3i 127	. . . . . . . 8 ⊢ (¬ M = ∅ → ¬ (M = ∅ ∧ X = ∅))
196		biorf 394	. . . . . . . 8 ⊢ (¬ (M = ∅ ∧ X = ∅) → ((⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∧ ¬ ⟪{M}, X⟫ ∈ ({{∅}} ×_k V)) ↔ ((M = ∅ ∧ X = ∅) ∨ (⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∧ ¬ ⟪{M}, X⟫ ∈ ({{∅}} ×_k V)))))
197	195, 196	syl 15	. . . . . . 7 ⊢ (¬ M = ∅ → ((⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∧ ¬ ⟪{M}, X⟫ ∈ ({{∅}} ×_k V)) ↔ ((M = ∅ ∧ X = ∅) ∨ (⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∧ ¬ ⟪{M}, X⟫ ∈ ({{∅}} ×_k V)))))
198	193, 197	bitrd 244	. . . . . 6 ⊢ (¬ M = ∅ → (⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ((M = ∅ ∧ X = ∅) ∨ (⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∧ ¬ ⟪{M}, X⟫ ∈ ({{∅}} ×_k V)))))
199	43, 3	opkelxpk 4248	. . . . . . . 8 ⊢ (⟪{M}, X⟫ ∈ ({{∅}} ×_k {∅}) ↔ ({M} ∈ {{∅}} ∧ X ∈ {∅}))
200	189, 6	anbi12i 678	. . . . . . . 8 ⊢ (({M} ∈ {{∅}} ∧ X ∈ {∅}) ↔ (M = ∅ ∧ X = ∅))
201	199, 200	bitri 240	. . . . . . 7 ⊢ (⟪{M}, X⟫ ∈ ({{∅}} ×_k {∅}) ↔ (M = ∅ ∧ X = ∅))
202		eldif 3221	. . . . . . 7 ⊢ (⟪{M}, X⟫ ∈ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)) ↔ (⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∧ ¬ ⟪{M}, X⟫ ∈ ({{∅}} ×_k V)))
203	201, 202	orbi12i 507	. . . . . 6 ⊢ ((⟪{M}, X⟫ ∈ ({{∅}} ×_k {∅}) ∨ ⟪{M}, X⟫ ∈ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ ((M = ∅ ∧ X = ∅) ∨ (⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∧ ¬ ⟪{M}, X⟫ ∈ ({{∅}} ×_k V))))
204	198, 203	syl6bbr 254	. . . . 5 ⊢ (¬ M = ∅ → (⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ↔ (⟪{M}, X⟫ ∈ ({{∅}} ×_k {∅}) ∨ ⟪{M}, X⟫ ∈ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
205		elun 3220	. . . . 5 ⊢ (⟪{M}, X⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ (⟪{M}, X⟫ ∈ ({{∅}} ×_k {∅}) ∨ ⟪{M}, X⟫ ∈ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))))
206	204, 205	syl6bbr 254	. . . 4 ⊢ (¬ M = ∅ → (⟪{M}, X⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ⟪{M}, X⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
207	26, 184, 206	3bitr2rd 273	. . 3 ⊢ (¬ M = ∅ → (⟪{M}, X⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ X = if(M = ∅, ∅, (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y)))))
208	24, 207	pm2.61i 156	. 2 ⊢ (⟪{M}, X⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ X = if(M = ∅, ∅, (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))))
209		df-tfin 4443	. . 3 ⊢ T_fin M = if(M = ∅, ∅, (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y)))
210	209	eqeq2i 2363	. 2 ⊢ (X = T_fin M ↔ X = if(M = ∅, ∅, (℩y(y ∈ Nn ∧ ∃a ∈ M ℘₁a ∈ y))))
211	208, 210	bitr4i 243	1 ⊢ (⟪{M}, X⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ 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)) “_k ℘₁℘₁℘₁1_c)) ⊕ Ins3_k I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ X = T_fin M)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 176 ∨ wo 357 ∧ wa 358 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 {cab 2339 ∃wrex 2615 Vcvv 2859 ∼ ccompl 3205 ∖ cdif 3206 ∪ cun 3207 ∩ cin 3208 ⊕ csymdif 3209 ∅c0 3550 ifcif 3662 ℘cpw 3722 {csn 3737 ∪cuni 3891 ⟪copk 4057 1_cc1c 4134 ℘₁cpw1 4135 ×_k cxpk 4174 ^◡_kccnvk 4175 Ins2_k cins2k 4176 Ins3_k cins3k 4177 “_k cimak 4179 SI_k csik 4181 S_k cssetk 4183 I_k cidk 4184 ℩cio 4337 Nn cnnc 4373 T_fin ctfin 4435

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 4078 ax-sn 4087

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-ne 2518 df-ral 2619 df-rex 2620 df-v 2861 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-symdif 3216 df-ss 3259 df-nul 3551 df-if 3663 df-pw 3724 df-sn 3741 df-pr 3742 df-uni 3892 df-opk 4058 df-1c 4136 df-pw1 4137 df-xpk 4185 df-cnvk 4186 df-ins2k 4187 df-ins3k 4188 df-imak 4189 df-sik 4192 df-ssetk 4193 df-idk 4195 df-iota 4339 df-tfin 4443

This theorem is referenced by: sfintfinlem1 4531 tfinnnlem1 4533 vfinspss 4551 vfinspclt 4552 vfinncsp 4554

W3C validator