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

Theorem sfintfinlem1 4531
Description: Lemma for sfintfin 4532. 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 2862 . . . . 5 m V
21eluni1 4173 . . . 4 (m 1 ∼ (k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) “k 1c) ↔ {m} ∼ (k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) “k 1c))
3 snex 4111 . . . . . . . 8 {m} V
43elimak 4259 . . . . . . 7 ({m} (k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) “k 1c) ↔ t 1ct, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)))
5 el1c 4139 . . . . . . . . . . 11 (t 1cn t = {n})
65anbi1i 676 . . . . . . . . . 10 ((t 1c t, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c))) ↔ (n t = {n} t, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “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 SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c))) ↔ (n t = {n} t, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c))))
86, 7bitr4i 243 . . . . . . . . 9 ((t 1c t, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c))) ↔ n(t = {n} t, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c))))
98exbii 1582 . . . . . . . 8 (t(t 1c t, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c))) ↔ tn(t = {n} t, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c))))
10 df-rex 2620 . . . . . . . 8 (t 1ct, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) ↔ t(t 1c t, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c))))
11 excom 1741 . . . . . . . 8 (nt(t = {n} t, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c))) ↔ tn(t = {n} t, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c))))
129, 10, 113bitr4i 268 . . . . . . 7 (t 1ct, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) ↔ nt(t = {n} t, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c))))
13 snex 4111 . . . . . . . . . 10 {n} V
14 opkeq1 4059 . . . . . . . . . . 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 SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) ↔ ⟪{n}, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c))))
1613, 15ceqsexv 2894 . . . . . . . . 9 (t(t = {n} t, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c))) ↔ ⟪{n}, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)))
1713, 3opkelcnvk 4250 . . . . . . . . 9 (⟪{n}, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) ↔ ⟪{m}, {n}⟫ ( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)))
18 eldif 3221 . . . . . . . . . 10 (⟪{m}, {n}⟫ ( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) ↔ (⟪{m}, {n}⟫ SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ¬ ⟪{m}, {n}⟫ (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)))
19 vex 2862 . . . . . . . . . . . . 13 n V
201, 19opksnelsik 4265 . . . . . . . . . . . 12 (⟪{m}, {n}⟫ SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ ⟪m, n (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))
211, 19srelk 4524 . . . . . . . . . . . 12 (⟪m, n (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ Sfin (m, n))
2220, 21bitri 240 . . . . . . . . . . 11 (⟪{m}, {n}⟫ SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ Sfin (m, n))
23 opkex 4113 . . . . . . . . . . . . . . 15 ⟪{m}, {n}⟫ V
2423elimak 4259 . . . . . . . . . . . . . 14 (⟪{m}, {n}⟫ (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c) ↔ t 1 1ct, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)))
25 df-rex 2620 . . . . . . . . . . . . . 14 (t 1 1ct, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) ↔ t(t 11c t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))))
26 elpw11c 4147 . . . . . . . . . . . . . . . . . 18 (t 11cy t = {{y}})
2726anbi1i 676 . . . . . . . . . . . . . . . . 17 ((t 11c t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))) ↔ (y t = {{y}} t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))))
28 19.41v 1901 . . . . . . . . . . . . . . . . 17 (y(t = {{y}} t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))) ↔ (y t = {{y}} t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))))
2927, 28bitr4i 243 . . . . . . . . . . . . . . . 16 ((t 11c t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))) ↔ y(t = {{y}} t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))))
3029exbii 1582 . . . . . . . . . . . . . . 15 (t(t 11c t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))) ↔ ty(t = {{y}} t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))))
31 excom 1741 . . . . . . . . . . . . . . 15 (yt(t = {{y}} t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))) ↔ ty(t = {{y}} t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))))
3230, 31bitr4i 243 . . . . . . . . . . . . . 14 (t(t 11c t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))) ↔ yt(t = {{y}} t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))))
3324, 25, 323bitri 262 . . . . . . . . . . . . 13 (⟪{m}, {n}⟫ (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c) ↔ yt(t = {{y}} t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))))
34 snex 4111 . . . . . . . . . . . . . . . 16 {{y}} V
35 opkeq1 4059 . . . . . . . . . . . . . . . . 17 (t = {{y}} → ⟪t, ⟪{m}, {n}⟫⟫ = ⟪{{y}}, ⟪{m}, {n}⟫⟫)
3635eleq1d 2419 . . . . . . . . . . . . . . . 16 (t = {{y}} → (⟪t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) ↔ ⟪{{y}}, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))))
3734, 36ceqsexv 2894 . . . . . . . . . . . . . . 15 (t(t = {{y}} t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))) ↔ ⟪{{y}}, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)))
38 elin 3219 . . . . . . . . . . . . . . 15 (⟪{{y}}, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) ↔ (⟪{{y}}, ⟪{m}, {n}⟫⟫ Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ⟪{{y}}, ⟪{m}, {n}⟫⟫ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)))
39 vex 2862 . . . . . . . . . . . . . . . . . 18 y V
4039, 3, 13otkelins2k 4255 . . . . . . . . . . . . . . . . 17 (⟪{{y}}, ⟪{m}, {n}⟫⟫ Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ ⟪y, {n}⟫ k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))))
4139, 13opkelcnvk 4250 . . . . . . . . . . . . . . . . 17 (⟪y, {n}⟫ k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ ⟪{n}, y (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))))
4219, 39eqtfinrelk 4486 . . . . . . . . . . . . . . . . 17 (⟪{n}, y (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ y = Tfin n)
4340, 41, 423bitri 262 . . . . . . . . . . . . . . . 16 (⟪{{y}}, ⟪{m}, {n}⟫⟫ Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ y = Tfin n)
4439, 3, 13otkelins3k 4256 . . . . . . . . . . . . . . . . 17 (⟪{{y}}, ⟪{m}, {n}⟫⟫ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c) ↔ ⟪y, {m}⟫ (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))
45 opkex 4113 . . . . . . . . . . . . . . . . . . 19 y, {m}⟫ V
4645elimak 4259 . . . . . . . . . . . . . . . . . 18 (⟪y, {m}⟫ (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c) ↔ t 1 1ct, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))))
47 elpw11c 4147 . . . . . . . . . . . . . . . . . . . . . 22 (t 11cx t = {{x}})
4847anbi1i 676 . . . . . . . . . . . . . . . . . . . . 21 ((t 11c t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))) ↔ (x t = {{x}} t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))))
49 19.41v 1901 . . . . . . . . . . . . . . . . . . . . 21 (x(t = {{x}} t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))) ↔ (x t = {{x}} t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))))
5048, 49bitr4i 243 . . . . . . . . . . . . . . . . . . . 20 ((t 11c t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))) ↔ x(t = {{x}} t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))))
5150exbii 1582 . . . . . . . . . . . . . . . . . . 19 (t(t 11c t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))) ↔ tx(t = {{x}} t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))))
52 df-rex 2620 . . . . . . . . . . . . . . . . . . 19 (t 1 1ct, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) ↔ t(t 11c t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))))
53 excom 1741 . . . . . . . . . . . . . . . . . . 19 (xt(t = {{x}} t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))) ↔ tx(t = {{x}} t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))))
5451, 52, 533bitr4i 268 . . . . . . . . . . . . . . . . . 18 (t 1 1ct, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) ↔ xt(t = {{x}} t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))))
55 snex 4111 . . . . . . . . . . . . . . . . . . . . 21 {{x}} V
56 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . 22 (t = {{x}} → ⟪t, ⟪y, {m}⟫⟫ = ⟪{{x}}, ⟪y, {m}⟫⟫)
5756eleq1d 2419 . . . . . . . . . . . . . . . . . . . . 21 (t = {{x}} → (⟪t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) ↔ ⟪{{x}}, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))))
5855, 57ceqsexv 2894 . . . . . . . . . . . . . . . . . . . 20 (t(t = {{x}} t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))) ↔ ⟪{{x}}, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))))
59 elin 3219 . . . . . . . . . . . . . . . . . . . 20 (⟪{{x}}, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) ↔ (⟪{{x}}, ⟪y, {m}⟫⟫ Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ⟪{{x}}, ⟪y, {m}⟫⟫ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))))
60 vex 2862 . . . . . . . . . . . . . . . . . . . . . . 23 x V
6160, 39, 3otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{{x}}, ⟪y, {m}⟫⟫ Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ ⟪x, {m}⟫ k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))))
6260, 3opkelcnvk 4250 . . . . . . . . . . . . . . . . . . . . . 22 (⟪x, {m}⟫ k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ ⟪{m}, x (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))))
631, 60eqtfinrelk 4486 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{m}, x (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ x = Tfin m)
6461, 62, 633bitri 262 . . . . . . . . . . . . . . . . . . . . 21 (⟪{{x}}, ⟪y, {m}⟫⟫ Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ x = Tfin m)
6560, 39, 3otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{{x}}, ⟪y, {m}⟫⟫ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ ⟪x, y (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))
6660, 39srelk 4524 . . . . . . . . . . . . . . . . . . . . . 22 (⟪x, y (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ Sfin (x, y))
6765, 66bitri 240 . . . . . . . . . . . . . . . . . . . . 21 (⟪{{x}}, ⟪y, {m}⟫⟫ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ Sfin (x, y))
6864, 67anbi12i 678 . . . . . . . . . . . . . . . . . . . 20 ((⟪{{x}}, ⟪y, {m}⟫⟫ Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ⟪{{x}}, ⟪y, {m}⟫⟫ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) ↔ (x = Tfin m Sfin (x, y)))
6958, 59, 683bitri 262 . . . . . . . . . . . . . . . . . . 19 (t(t = {{x}} t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))) ↔ (x = Tfin m Sfin (x, y)))
7069exbii 1582 . . . . . . . . . . . . . . . . . 18 (xt(t = {{x}} t, ⟪y, {m}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))) ↔ x(x = Tfin m Sfin (x, y)))
7146, 54, 703bitri 262 . . . . . . . . . . . . . . . . 17 (⟪y, {m}⟫ (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c) ↔ x(x = Tfin m Sfin (x, y)))
72 tfinex 4485 . . . . . . . . . . . . . . . . . 18 Tfin m V
73 sfineq1 4526 . . . . . . . . . . . . . . . . . 18 (x = Tfin m → ( Sfin (x, y) ↔ Sfin ( Tfin m, y)))
7472, 73ceqsexv 2894 . . . . . . . . . . . . . . . . 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 SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c) ↔ Sfin ( Tfin m, y))
7643, 75anbi12i 678 . . . . . . . . . . . . . . 15 ((⟪{{y}}, ⟪{m}, {n}⟫⟫ Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ⟪{{y}}, ⟪{m}, {n}⟫⟫ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) ↔ (y = Tfin n Sfin ( Tfin m, y)))
7737, 38, 763bitri 262 . . . . . . . . . . . . . 14 (t(t = {{y}} t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))) ↔ (y = Tfin n Sfin ( Tfin m, y)))
7877exbii 1582 . . . . . . . . . . . . 13 (yt(t = {{y}} t, ⟪{m}, {n}⟫⟫ ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c))) ↔ y(y = Tfin n Sfin ( Tfin m, y)))
79 tfinex 4485 . . . . . . . . . . . . . 14 Tfin n V
80 sfineq2 4527 . . . . . . . . . . . . . 14 (y = Tfin n → ( Sfin ( Tfin m, y) ↔ Sfin ( Tfin m, Tfin n)))
8179, 80ceqsexv 2894 . . . . . . . . . . . . 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 SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c) ↔ Sfin ( Tfin m, Tfin n))
8382notbii 287 . . . . . . . . . . 11 (¬ ⟪{m}, {n}⟫ (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “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 SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ¬ ⟪{m}, {n}⟫ (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “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 SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “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 SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c))) ↔ ¬ ( Sfin (m, n) → Sfin ( Tfin m, Tfin n)))
8887exbii 1582 . . . . . . 7 (nt(t = {n} t, {m}⟫ k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “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 SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “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 SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) “k 1c) ↔ ¬ n ¬ ( Sfin (m, n) → Sfin ( Tfin m, Tfin n)))
913elcompl 3225 . . . . 5 ({m} ∼ (k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) “k 1c) ↔ ¬ {m} (k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “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 SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “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 SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) “k 1c) ↔ n( Sfin (m, n) → Sfin ( Tfin m, Tfin n)))
9594abbi2i 2464 . 2 1 ∼ (k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) “k 1c) = {m n( Sfin (m, n) → Sfin ( Tfin m, Tfin n))}
96 srelkex 4525 . . . . . . . 8 (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) V
9796sikex 4297 . . . . . . 7 SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) V
98 tfinrelkex 4487 . . . . . . . . . . 11 (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) V
9998cnvkex 4287 . . . . . . . . . 10 k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) V
10099ins2kex 4307 . . . . . . . . 9 Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) V
10196ins3kex 4308 . . . . . . . . . . . 12 Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) V
102100, 101inex 4105 . . . . . . . . . . 11 ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) V
103 1cex 4142 . . . . . . . . . . . 12 1c V
104103pw1ex 4303 . . . . . . . . . . 11 11c V
105102, 104imakex 4300 . . . . . . . . . 10 (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c) V
106105ins3kex 4308 . . . . . . . . 9 Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c) V
107100, 106inex 4105 . . . . . . . 8 ( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) V
108107, 104imakex 4300 . . . . . . 7 (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c) V
10997, 108difex 4107 . . . . . 6 ( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) V
110109cnvkex 4287 . . . . 5 k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) V
111110, 103imakex 4300 . . . 4 (k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) “k 1c) V
112111complex 4104 . . 3 ∼ (k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “k 11c)) “k 11c)) “k 1c) V
113112uni1ex 4293 . 2 1 ∼ (k( SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Ins2k k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ∩ Ins3k (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c))) “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
Syntax hints:  ¬ wn 3  wi 4   wa 358  wal 1540  wex 1541   = wceq 1642   wcel 1710  {cab 2339  wrex 2615  Vcvv 2859  ccompl 3205   cdif 3206  cun 3207  cin 3208  csymdif 3209  c0 3550  cpw 3722  {csn 3737  copk 4057  1cuni1 4133  1cc1c 4134  1cpw1 4135   ×k cxpk 4174  kccnvk 4175   Ins2k cins2k 4176   Ins3k cins3k 4177  k cimak 4179   SIk csik 4181   Sk cssetk 4183   Ik cidk 4184   Nn cnnc 4373   Tfin ctfin 4435   Sfin wsfin 4438
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-addc 4378  df-nnc 4379  df-tfin 4443  df-sfin 4446
This theorem is referenced by:  sfintfin  4532
  Copyright terms: Public domain W3C validator