nnpweqlem1 - New Foundations Explorer

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

Theorem nnpweqlem1 4523

Description: Lemma for nnpweq 4524. Establish stratification for induction. (Contributed by SF, 26-Jan-2015.)

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

Distinct variable group: m,a,b,n

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

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

W3C validator