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

Theorem sfintfinlem1 4532
Description: Lemma for sfintfin 4533. Set up induction stratification. (Contributed by SF, 31-Jan-2015.)
Assertion
Ref Expression
sfintfinlem1 ⊢ {m ∣ ∀n( Sfin (m, n) → Sfin ( Tfin m, Tfin n))} ∈ V
Distinct variable group:   m,n

Proof of Theorem sfintfinlem1
Dummy variables t x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2863 . . . . 5 ⊢ m ∈ V
21eluni1 4174 . . . 4 ⊢ (m ∈ ⋃1 ∼ (◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) “k 1c) ↔ {m} ∈ ∼ (◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) “k 1c))
3 snex 4112 . . . . . . . 8 ⊢ {m} ∈ V
43elimak 4260 . . . . . . 7 ⊢ ({m} ∈ (◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) “k 1c) ↔ ∃t ∈ 1c ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)))
5 el1c 4140 . . . . . . . . . . 11 ⊢ (t ∈ 1c ↔ ∃n t = {n})
65anbi1i 676 . . . . . . . . . 10 ⊢ ((t ∈ 1c ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))) ↔ (∃n t = {n} ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))))
7 19.41v 1901 . . . . . . . . . 10 ⊢ (∃n(t = {n} ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))) ↔ (∃n t = {n} ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))))
86, 7bitr4i 243 . . . . . . . . 9 ⊢ ((t ∈ 1c ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))) ↔ ∃n(t = {n} ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))))
98exbii 1582 . . . . . . . 8 ⊢ (∃t(t ∈ 1c ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))) ↔ ∃t∃n(t = {n} ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))))
10 df-rex 2621 . . . . . . . 8 ⊢ (∃t ∈ 1c ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) ↔ ∃t(t ∈ 1c ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))))
11 excom 1741 . . . . . . . 8 ⊢ (∃n∃t(t = {n} ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))) ↔ ∃t∃n(t = {n} ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))))
129, 10, 113bitr4i 268 . . . . . . 7 ⊢ (∃t ∈ 1c ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) ↔ ∃n∃t(t = {n} ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))))
13 snex 4112 . . . . . . . . . 10 ⊢ {n} ∈ V
14 opkeq1 4060 . . . . . . . . . . 11 ⊢ (t = {n} → ⟪t, {m}⟫ = ⟪{n}, {m}⟫)
1514eleq1d 2419 . . . . . . . . . 10 ⊢ (t = {n} → (⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) ↔ ⟪{n}, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))))
1613, 15ceqsexv 2895 . . . . . . . . 9 ⊢ (∃t(t = {n} ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))) ↔ ⟪{n}, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)))
1713, 3opkelcnvk 4251 . . . . . . . . 9 ⊢ (⟪{n}, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) ↔ ⟪{m}, {n}⟫ ∈ ( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)))
18 eldif 3222 . . . . . . . . . 10 ⊢ (⟪{m}, {n}⟫ ∈ ( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) ↔ (⟪{m}, {n}⟫ ∈ SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∧ ¬ ⟪{m}, {n}⟫ ∈ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)))
19 vex 2863 . . . . . . . . . . . . 13 ⊢ n ∈ V
201, 19opksnelsik 4266 . . . . . . . . . . . 12 ⊢ (⟪{m}, {n}⟫ ∈ SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ↔ ⟪m, n⟫ ∈ (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))
211, 19srelk 4525 . . . . . . . . . . . 12 ⊢ (⟪m, n⟫ ∈ (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ↔ Sfin (m, n))
2220, 21bitri 240 . . . . . . . . . . 11 ⊢ (⟪{m}, {n}⟫ ∈ SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ↔ Sfin (m, n))
23 opkex 4114 . . . . . . . . . . . . . . 15 ⊢ ⟪{m}, {n}⟫ ∈ V
2423elimak 4260 . . . . . . . . . . . . . 14 ⊢ (⟪{m}, {n}⟫ ∈ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c) ↔ ∃t ∈ ℘1 1c⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)))
25 df-rex 2621 . . . . . . . . . . . . . 14 ⊢ (∃t ∈ ℘1 1c⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) ↔ ∃t(t ∈ ℘11c ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))))
26 elpw11c 4148 . . . . . . . . . . . . . . . . . 18 ⊢ (t ∈ ℘11c ↔ ∃y t = {{y}})
2726anbi1i 676 . . . . . . . . . . . . . . . . 17 ⊢ ((t ∈ ℘11c ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))) ↔ (∃y t = {{y}} ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))))
28 19.41v 1901 . . . . . . . . . . . . . . . . 17 ⊢ (∃y(t = {{y}} ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))) ↔ (∃y t = {{y}} ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))))
2927, 28bitr4i 243 . . . . . . . . . . . . . . . 16 ⊢ ((t ∈ ℘11c ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))) ↔ ∃y(t = {{y}} ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))))
3029exbii 1582 . . . . . . . . . . . . . . 15 ⊢ (∃t(t ∈ ℘11c ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))) ↔ ∃t∃y(t = {{y}} ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))))
31 excom 1741 . . . . . . . . . . . . . . 15 ⊢ (∃y∃t(t = {{y}} ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))) ↔ ∃t∃y(t = {{y}} ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))))
3230, 31bitr4i 243 . . . . . . . . . . . . . 14 ⊢ (∃t(t ∈ ℘11c ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))) ↔ ∃y∃t(t = {{y}} ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))))
3324, 25, 323bitri 262 . . . . . . . . . . . . 13 ⊢ (⟪{m}, {n}⟫ ∈ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c) ↔ ∃y∃t(t = {{y}} ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))))
34 snex 4112 . . . . . . . . . . . . . . . 16 ⊢ {{y}} ∈ V
35 opkeq1 4060 . . . . . . . . . . . . . . . . 17 ⊢ (t = {{y}} → ⟪t, ⟪{m}, {n}⟫⟫ = ⟪{{y}}, ⟪{m}, {n}⟫⟫)
3635eleq1d 2419 . . . . . . . . . . . . . . . 16 ⊢ (t = {{y}} → (⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) ↔ ⟪{{y}}, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))))
3734, 36ceqsexv 2895 . . . . . . . . . . . . . . 15 ⊢ (∃t(t = {{y}} ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))) ↔ ⟪{{y}}, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)))
38 elin 3220 . . . . . . . . . . . . . . 15 ⊢ (⟪{{y}}, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) ↔ (⟪{{y}}, ⟪{m}, {n}⟫⟫ ∈ Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∧ ⟪{{y}}, ⟪{m}, {n}⟫⟫ ∈ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)))
39 vex 2863 . . . . . . . . . . . . . . . . . 18 ⊢ y ∈ V
4039, 3, 13otkelins2k 4256 . . . . . . . . . . . . . . . . 17 ⊢ (⟪{{y}}, ⟪{m}, {n}⟫⟫ ∈ Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ↔ ⟪y, {n}⟫ ∈ ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))))
4139, 13opkelcnvk 4251 . . . . . . . . . . . . . . . . 17 ⊢ (⟪y, {n}⟫ ∈ ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ↔ ⟪{n}, y⟫ ∈ (({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))))
4219, 39eqtfinrelk 4487 . . . . . . . . . . . . . . . . 17 ⊢ (⟪{n}, y⟫ ∈ (({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ↔ y = Tfin n)
4340, 41, 423bitri 262 . . . . . . . . . . . . . . . 16 ⊢ (⟪{{y}}, ⟪{m}, {n}⟫⟫ ∈ Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ↔ y = Tfin n)
4439, 3, 13otkelins3k 4257 . . . . . . . . . . . . . . . . 17 ⊢ (⟪{{y}}, ⟪{m}, {n}⟫⟫ ∈ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c) ↔ ⟪y, {m}⟫ ∈ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))
45 opkex 4114 . . . . . . . . . . . . . . . . . . 19 ⊢ ⟪y, {m}⟫ ∈ V
4645elimak 4260 . . . . . . . . . . . . . . . . . 18 ⊢ (⟪y, {m}⟫ ∈ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c) ↔ ∃t ∈ ℘1 1c⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))))
47 elpw11c 4148 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (t ∈ ℘11c ↔ ∃x t = {{x}})
4847anbi1i 676 . . . . . . . . . . . . . . . . . . . . 21 ⊢ ((t ∈ ℘11c ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))) ↔ (∃x t = {{x}} ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))))
49 19.41v 1901 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃x(t = {{x}} ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))) ↔ (∃x t = {{x}} ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))))
5048, 49bitr4i 243 . . . . . . . . . . . . . . . . . . . 20 ⊢ ((t ∈ ℘11c ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))) ↔ ∃x(t = {{x}} ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))))
5150exbii 1582 . . . . . . . . . . . . . . . . . . 19 ⊢ (∃t(t ∈ ℘11c ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))) ↔ ∃t∃x(t = {{x}} ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))))
52 df-rex 2621 . . . . . . . . . . . . . . . . . . 19 ⊢ (∃t ∈ ℘1 1c⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) ↔ ∃t(t ∈ ℘11c ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))))
53 excom 1741 . . . . . . . . . . . . . . . . . . 19 ⊢ (∃x∃t(t = {{x}} ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))) ↔ ∃t∃x(t = {{x}} ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))))
5451, 52, 533bitr4i 268 . . . . . . . . . . . . . . . . . 18 ⊢ (∃t ∈ ℘1 1c⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) ↔ ∃x∃t(t = {{x}} ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))))
55 snex 4112 . . . . . . . . . . . . . . . . . . . . 21 ⊢ {{x}} ∈ V
56 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (t = {{x}} → ⟪t, ⟪y, {m}⟫⟫ = ⟪{{x}}, ⟪y, {m}⟫⟫)
5756eleq1d 2419 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (t = {{x}} → (⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) ↔ ⟪{{x}}, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))))
5855, 57ceqsexv 2895 . . . . . . . . . . . . . . . . . . . 20 ⊢ (∃t(t = {{x}} ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))) ↔ ⟪{{x}}, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))))
59 elin 3220 . . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{{x}}, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) ↔ (⟪{{x}}, ⟪y, {m}⟫⟫ ∈ Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∧ ⟪{{x}}, ⟪y, {m}⟫⟫ ∈ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))))
60 vex 2863 . . . . . . . . . . . . . . . . . . . . . . 23 ⊢ x ∈ V
6160, 39, 3otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟪{{x}}, ⟪y, {m}⟫⟫ ∈ Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ↔ ⟪x, {m}⟫ ∈ ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))))
6260, 3opkelcnvk 4251 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟪x, {m}⟫ ∈ ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ↔ ⟪{m}, x⟫ ∈ (({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))))
631, 60eqtfinrelk 4487 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟪{m}, x⟫ ∈ (({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ↔ x = Tfin m)
6461, 62, 633bitri 262 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟪{{x}}, ⟪y, {m}⟫⟫ ∈ Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ↔ x = Tfin m)
6560, 39, 3otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟪{{x}}, ⟪y, {m}⟫⟫ ∈ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ↔ ⟪x, y⟫ ∈ (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))
6660, 39srelk 4525 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟪x, y⟫ ∈ (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ↔ Sfin (x, y))
6765, 66bitri 240 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟪{{x}}, ⟪y, {m}⟫⟫ ∈ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ↔ Sfin (x, y))
6864, 67anbi12i 678 . . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟪{{x}}, ⟪y, {m}⟫⟫ ∈ Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∧ ⟪{{x}}, ⟪y, {m}⟫⟫ ∈ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) ↔ (x = Tfin m ∧ Sfin (x, y)))
6958, 59, 683bitri 262 . . . . . . . . . . . . . . . . . . 19 ⊢ (∃t(t = {{x}} ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))) ↔ (x = Tfin m ∧ Sfin (x, y)))
7069exbii 1582 . . . . . . . . . . . . . . . . . 18 ⊢ (∃x∃t(t = {{x}} ∧ ⟪t, ⟪y, {m}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)))) ↔ ∃x(x = Tfin m ∧ Sfin (x, y)))
7146, 54, 703bitri 262 . . . . . . . . . . . . . . . . 17 ⊢ (⟪y, {m}⟫ ∈ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c) ↔ ∃x(x = Tfin m ∧ Sfin (x, y)))
72 tfinex 4486 . . . . . . . . . . . . . . . . . 18 ⊢ Tfin m ∈ V
73 sfineq1 4527 . . . . . . . . . . . . . . . . . 18 ⊢ (x = Tfin m → ( Sfin (x, y) ↔ Sfin ( Tfin m, y)))
7472, 73ceqsexv 2895 . . . . . . . . . . . . . . . . 17 ⊢ (∃x(x = Tfin m ∧ Sfin (x, y)) ↔ Sfin ( Tfin m, y))
7544, 71, 743bitri 262 . . . . . . . . . . . . . . . 16 ⊢ (⟪{{y}}, ⟪{m}, {n}⟫⟫ ∈ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c) ↔ Sfin ( Tfin m, y))
7643, 75anbi12i 678 . . . . . . . . . . . . . . 15 ⊢ ((⟪{{y}}, ⟪{m}, {n}⟫⟫ ∈ Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∧ ⟪{{y}}, ⟪{m}, {n}⟫⟫ ∈ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) ↔ (y = Tfin n ∧ Sfin ( Tfin m, y)))
7737, 38, 763bitri 262 . . . . . . . . . . . . . 14 ⊢ (∃t(t = {{y}} ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))) ↔ (y = Tfin n ∧ Sfin ( Tfin m, y)))
7877exbii 1582 . . . . . . . . . . . . 13 ⊢ (∃y∃t(t = {{y}} ∧ ⟪t, ⟪{m}, {n}⟫⟫ ∈ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c))) ↔ ∃y(y = Tfin n ∧ Sfin ( Tfin m, y)))
79 tfinex 4486 . . . . . . . . . . . . . 14 ⊢ Tfin n ∈ V
80 sfineq2 4528 . . . . . . . . . . . . . 14 ⊢ (y = Tfin n → ( Sfin ( Tfin m, y) ↔ Sfin ( Tfin m, Tfin n)))
8179, 80ceqsexv 2895 . . . . . . . . . . . . 13 ⊢ (∃y(y = Tfin n ∧ Sfin ( Tfin m, y)) ↔ Sfin ( Tfin m, Tfin n))
8233, 78, 813bitri 262 . . . . . . . . . . . 12 ⊢ (⟪{m}, {n}⟫ ∈ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c) ↔ Sfin ( Tfin m, Tfin n))
8382notbii 287 . . . . . . . . . . 11 ⊢ (¬ ⟪{m}, {n}⟫ ∈ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c) ↔ ¬ Sfin ( Tfin m, Tfin n))
8422, 83anbi12i 678 . . . . . . . . . 10 ⊢ ((⟪{m}, {n}⟫ ∈ SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∧ ¬ ⟪{m}, {n}⟫ ∈ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) ↔ ( Sfin (m, n) ∧ ¬ Sfin ( Tfin m, Tfin n)))
85 annim 414 . . . . . . . . . 10 ⊢ (( Sfin (m, n) ∧ ¬ Sfin ( Tfin m, Tfin n)) ↔ ¬ ( Sfin (m, n) → Sfin ( Tfin m, Tfin n)))
8618, 84, 853bitri 262 . . . . . . . . 9 ⊢ (⟪{m}, {n}⟫ ∈ ( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) ↔ ¬ ( Sfin (m, n) → Sfin ( Tfin m, Tfin n)))
8716, 17, 863bitri 262 . . . . . . . 8 ⊢ (∃t(t = {n} ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))) ↔ ¬ ( Sfin (m, n) → Sfin ( Tfin m, Tfin n)))
8887exbii 1582 . . . . . . 7 ⊢ (∃n∃t(t = {n} ∧ ⟪t, {m}⟫ ∈ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c))) ↔ ∃n ¬ ( Sfin (m, n) → Sfin ( Tfin m, Tfin n)))
894, 12, 883bitri 262 . . . . . 6 ⊢ ({m} ∈ (◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) “k 1c) ↔ ∃n ¬ ( Sfin (m, n) → Sfin ( Tfin m, Tfin n)))
9089notbii 287 . . . . 5 ⊢ (¬ {m} ∈ (◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) “k 1c) ↔ ¬ ∃n ¬ ( Sfin (m, n) → Sfin ( Tfin m, Tfin n)))
913elcompl 3226 . . . . 5 ⊢ ({m} ∈ ∼ (◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) “k 1c) ↔ ¬ {m} ∈ (◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) “k 1c))
92 alex 1572 . . . . 5 ⊢ (∀n( Sfin (m, n) → Sfin ( Tfin m, Tfin n)) ↔ ¬ ∃n ¬ ( Sfin (m, n) → Sfin ( Tfin m, Tfin n)))
9390, 91, 923bitr4i 268 . . . 4 ⊢ ({m} ∈ ∼ (◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) “k 1c) ↔ ∀n( Sfin (m, n) → Sfin ( Tfin m, Tfin n)))
942, 93bitri 240 . . 3 ⊢ (m ∈ ⋃1 ∼ (◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) “k 1c) ↔ ∀n( Sfin (m, n) → Sfin ( Tfin m, Tfin n)))
9594eqabi 2465 . 2 ⊢ ⋃1 ∼ (◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) “k 1c) = {m ∣ ∀n( Sfin (m, n) → Sfin ( Tfin m, Tfin n))}
96 srelkex 4526 . . . . . . . 8 ⊢ (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∈ V
9796sikex 4298 . . . . . . 7 ⊢ SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∈ V
98 tfinrelkex 4488 . . . . . . . . . . 11 ⊢ (({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∈ V
9998cnvkex 4288 . . . . . . . . . 10 ⊢ ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∈ V
10099ins2kex 4308 . . . . . . . . 9 ⊢ Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∈ V
10196ins3kex 4309 . . . . . . . . . . . 12 ⊢ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∈ V
102100, 101inex 4106 . . . . . . . . . . 11 ⊢ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) ∈ V
103 1cex 4143 . . . . . . . . . . . 12 ⊢ 1c ∈ V
104103pw1ex 4304 . . . . . . . . . . 11 ⊢ ℘11c ∈ V
105102, 104imakex 4301 . . . . . . . . . 10 ⊢ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c) ∈ V
106105ins3kex 4309 . . . . . . . . 9 ⊢ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c) ∈ V
107100, 106inex 4106 . . . . . . . 8 ⊢ ( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) ∈ V
108107, 104imakex 4301 . . . . . . 7 ⊢ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c) ∈ V
10997, 108difex 4108 . . . . . 6 ⊢ ( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) ∈ V
110109cnvkex 4288 . . . . 5 ⊢ ◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) ∈ V
111110, 103imakex 4301 . . . 4 ⊢ (◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) “k 1c) ∈ V
112111complex 4105 . . 3 ⊢ ∼ (◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) “k 1c) ∈ V
113112uni1ex 4294 . 2 ⊢ ⋃1 ∼ (◡k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∖ (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Ins2k ◡k(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c))) “k ℘11c)) “k ℘11c)) “k 1c) ∈ V
11495, 113eqeltrri 2424 1 ⊢ {m ∣ ∀n( Sfin (m, n) → Sfin ( Tfin m, Tfin 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   ∪ cun 3208   ∩ cin 3209   ⊕ csymdif 3210  ∅c0 3551  ℘cpw 3723  {csn 3738  ⟪copk 4058  ⋃1cuni1 4134  1cc1c 4135  ℘1cpw1 4136   ×k cxpk 4175  ◡kccnvk 4176   Ins2k cins2k 4177   Ins3k cins3k 4178   “k cimak 4180   SIk csik 4182   Sk cssetk 4184   Ik cidk 4185   Nn cnnc 4374   Tfin ctfin 4436   Sfin wsfin 4439
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-eu 2208  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-idk 4196  df-iota 4340  df-addc 4379  df-nnc 4380  df-tfin 4444  df-sfin 4447
This theorem is used by:  sfintfin  4533
  Copyright terms: Public domain W3C validator