ncfinlowerlem1 - New Foundations Explorer

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

Theorem ncfinlowerlem1 4483

Description: Lemma for ncfinlower 4484. Set up stratification for induction. (Contributed by SF, 22-Jan-2015.)

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

Distinct variable group: m,n,a,b

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

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 358 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 {cab 2339 ∃wrex 2616 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ∩ cin 3209 ⊕ csymdif 3210 ℘cpw 3723 {csn 3738 ⟪copk 4058 1_cc1c 4135 ℘₁cpw1 4136 ×_k cxpk 4175 ^◡_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 proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4079 ax-xp 4080 ax-cnv 4081 ax-1c 4082 ax-sset 4083 ax-si 4084 ax-ins2 4085 ax-ins3 4086 ax-typlower 4087 ax-sn 4088

This proof depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-v 2862 df-sbc 3048 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-nul 3552 df-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-uni1 4139 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-p6 4192 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-addc 4379 df-nnc 4380

This theorem is used by: ncfinlower 4484

W3C validator