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

Theorem tfinnnlem1 4534
Description: Lemma for tfinnn 4535. Establish stratification. (Contributed by SF, 30-Jan-2015.)
Assertion
Ref Expression
tfinnnlem1 {n y n (y Nn → {a x y a = Tfin x} Tfin n)} V
Distinct variable group:   y,n,a,x

Proof of Theorem tfinnnlem1
Dummy variables t w z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2863 . . . . 5 n V
21eluni1 4174 . . . 4 (n 1 ∼ (( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) “k 11c) ↔ {n} ∼ (( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) “k 11c))
3 snex 4112 . . . . . . . . . 10 {{y}} V
4 opkeq1 4060 . . . . . . . . . . 11 (t = {{y}} → ⟪t, {n}⟫ = ⟪{{y}}, {n}⟫)
54eleq1d 2419 . . . . . . . . . 10 (t = {{y}} → (⟪t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) ↔ ⟪{{y}}, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))))
63, 5ceqsexv 2895 . . . . . . . . 9 (t(t = {{y}} t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))) ↔ ⟪{{y}}, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))))
7 elin 3220 . . . . . . . . 9 (⟪{{y}}, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) ↔ (⟪{{y}}, {n}⟫ SIk Sk ⟪{{y}}, {n}⟫ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))))
8 snex 4112 . . . . . . . . . . . 12 {y} V
98, 1opksnelsik 4266 . . . . . . . . . . 11 (⟪{{y}}, {n}⟫ SIk Sk ↔ ⟪{y}, n Sk )
10 vex 2863 . . . . . . . . . . . 12 y V
1110, 1elssetk 4271 . . . . . . . . . . 11 (⟪{y}, n Sky n)
129, 11bitri 240 . . . . . . . . . 10 (⟪{{y}}, {n}⟫ SIk Sky n)
13 eldif 3222 . . . . . . . . . . 11 (⟪{{y}}, {n}⟫ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)) ↔ (⟪{{y}}, {n}⟫ SIk (1 Nn ×k V) ¬ ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))
148, 1opksnelsik 4266 . . . . . . . . . . . . 13 (⟪{{y}}, {n}⟫ SIk (1 Nn ×k V) ↔ ⟪{y}, n (1 Nn ×k V))
158, 1opkelxpk 4249 . . . . . . . . . . . . . . 15 (⟪{y}, n (1 Nn ×k V) ↔ ({y} 1 Nn n V))
161, 15mpbiran2 885 . . . . . . . . . . . . . 14 (⟪{y}, n (1 Nn ×k V) ↔ {y} 1 Nn )
17 snelpw1 4147 . . . . . . . . . . . . . 14 ({y} 1 Nny Nn )
1816, 17bitri 240 . . . . . . . . . . . . 13 (⟪{y}, n (1 Nn ×k V) ↔ y Nn )
1910elpw 3729 . . . . . . . . . . . . 13 (y Nny Nn )
2014, 18, 193bitri 262 . . . . . . . . . . . 12 (⟪{{y}}, {n}⟫ SIk (1 Nn ×k V) ↔ y Nn )
21 snex 4112 . . . . . . . . . . . . . . . . 17 {{z}} V
22 opkeq1 4060 . . . . . . . . . . . . . . . . . 18 (t = {{z}} → ⟪t, ⟪{{y}}, {n}⟫⟫ = ⟪{{z}}, ⟪{{y}}, {n}⟫⟫)
2322eleq1d 2419 . . . . . . . . . . . . . . . . 17 (t = {{z}} → (⟪t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) ↔ ⟪{{z}}, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))))
2421, 23ceqsexv 2895 . . . . . . . . . . . . . . . 16 (t(t = {{z}} t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ ⟪{{z}}, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)))
25 elin 3220 . . . . . . . . . . . . . . . 16 (⟪{{z}}, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) ↔ (⟪{{z}}, ⟪{{y}}, {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))) ⟪{{z}}, ⟪{{y}}, {n}⟫⟫ Ins3k (( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)))
26 vex 2863 . . . . . . . . . . . . . . . . . . 19 z V
27 snex 4112 . . . . . . . . . . . . . . . . . . 19 {n} V
2826, 3, 27otkelins2k 4256 . . . . . . . . . . . . . . . . . 18 (⟪{{z}}, ⟪{{y}}, {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))) ↔ ⟪z, {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))))
2926, 27opkelcnvk 4251 . . . . . . . . . . . . . . . . . 18 (⟪z, {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}, z (({{}} ×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))))
301, 26eqtfinrelk 4487 . . . . . . . . . . . . . . . . . 18 (⟪{n}, z (({{}} ×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))) ↔ z = Tfin n)
3128, 29, 303bitri 262 . . . . . . . . . . . . . . . . 17 (⟪{{z}}, ⟪{{y}}, {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))) ↔ z = Tfin n)
32 opkex 4114 . . . . . . . . . . . . . . . . . . . 20 z, {{y}}⟫ V
3332elimak 4260 . . . . . . . . . . . . . . . . . . 19 (⟪z, {{y}}⟫ (( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c) ↔ t 1 11ct, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ))
34 elpw121c 4149 . . . . . . . . . . . . . . . . . . . . . . 23 (t 111cw t = {{{w}}})
3534anbi1i 676 . . . . . . . . . . . . . . . . . . . . . 22 ((t 111c t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )) ↔ (w t = {{{w}}} t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )))
36 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . 22 (w(t = {{{w}}} t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )) ↔ (w t = {{{w}}} t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )))
3735, 36bitr4i 243 . . . . . . . . . . . . . . . . . . . . 21 ((t 111c t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )) ↔ w(t = {{{w}}} t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )))
3837exbii 1582 . . . . . . . . . . . . . . . . . . . 20 (t(t 111c t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )) ↔ tw(t = {{{w}}} t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )))
39 df-rex 2621 . . . . . . . . . . . . . . . . . . . 20 (t 1 11ct, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) ↔ t(t 111c t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )))
40 excom 1741 . . . . . . . . . . . . . . . . . . . 20 (wt(t = {{{w}}} t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )) ↔ tw(t = {{{w}}} t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )))
4138, 39, 403bitr4i 268 . . . . . . . . . . . . . . . . . . 19 (t 1 11ct, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) ↔ wt(t = {{{w}}} t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )))
42 snex 4112 . . . . . . . . . . . . . . . . . . . . . 22 {{{w}}} V
43 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . 23 (t = {{{w}}} → ⟪t, ⟪z, {{y}}⟫⟫ = ⟪{{{w}}}, ⟪z, {{y}}⟫⟫)
4443eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . 22 (t = {{{w}}} → (⟪t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) ↔ ⟪{{{w}}}, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )))
4542, 44ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . 21 (t(t = {{{w}}} t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )) ↔ ⟪{{{w}}}, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ))
46 elin 3220 . . . . . . . . . . . . . . . . . . . . 21 (⟪{{{w}}}, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) ↔ (⟪{{{w}}}, ⟪z, {{y}}⟫⟫ Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ⟪{{{w}}}, ⟪z, {{y}}⟫⟫ Ins3k Sk ))
47 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . 24 {w} V
4847, 26, 3otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{{w}}}, ⟪z, {{y}}⟫⟫ Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ↔ ⟪{w}, {{y}}⟫ SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c))
49 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . 24 w V
5049, 8opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{w}, {{y}}⟫ SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ↔ ⟪w, {y}⟫ ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c))
51 opkex 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 w, {y}⟫ V
5251elimak 4260 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪w, {y}⟫ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ↔ t 1 11ct, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)))
53 elpw121c 4149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t 111ca t = {{{a}}})
5453anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((t 111c t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))) ↔ (a t = {{{a}}} t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))))
55 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (a(t = {{{a}}} t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))) ↔ (a t = {{{a}}} t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))))
5654, 55bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((t 111c t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))) ↔ a(t = {{{a}}} t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))))
5756exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (t(t 111c t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))) ↔ ta(t = {{{a}}} t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))))
58 df-rex 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (t 1 11ct, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) ↔ t(t 111c t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))))
59 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (at(t = {{{a}}} t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))) ↔ ta(t = {{{a}}} t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))))
6057, 58, 593bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (t 1 11ct, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) ↔ at(t = {{{a}}} t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))))
61 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 {{{a}}} V
62 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t = {{{a}}} → ⟪t, ⟪w, {y}⟫⟫ = ⟪{{{a}}}, ⟪w, {y}⟫⟫)
6362eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t = {{{a}}} → (⟪t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) ↔ ⟪{{{a}}}, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))))
6461, 63ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t(t = {{{a}}} t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))) ↔ ⟪{{{a}}}, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)))
65 elsymdif 3224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪{{{a}}}, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) ↔ ¬ (⟪{{{a}}}, ⟪w, {y}⟫⟫ Ins3k Sk ↔ ⟪{{{a}}}, ⟪w, {y}⟫⟫ Ins2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)))
66 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 {a} V
6766, 49, 8otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{a}}}, ⟪w, {y}⟫⟫ Ins3k Sk ↔ ⟪{a}, w Sk )
68 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 a V
6968, 49elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{a}, w Ska w)
7067, 69bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{a}}}, ⟪w, {y}⟫⟫ Ins3k Ska w)
7166, 49, 8otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{a}}}, ⟪w, {y}⟫⟫ Ins2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c) ↔ ⟪{a}, {y}⟫ SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))
72 opkex 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 a, y V
7372elimak 4260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪a, y (( Ins2k SkIns3k (({{}} ×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)))) “k 111c) ↔ t 1 11ct, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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)))))
74 elpw121c 4149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (t 111cx t = {{{x}}})
7574anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((t 111c t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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 t = {{{x}}} t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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))))))
76 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (x(t = {{{x}}} t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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 t = {{{x}}} t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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))))))
7775, 76bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((t 111c t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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(t = {{{x}}} t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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))))))
7877exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t(t 111c t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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))))) ↔ tx(t = {{{x}}} t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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))))))
79 df-rex 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t 1 11ct, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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)))) ↔ t(t 111c t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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))))))
80 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (xt(t = {{{x}}} t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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))))) ↔ tx(t = {{{x}}} t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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))))))
8178, 79, 803bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (t 1 11ct, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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)))) ↔ xt(t = {{{x}}} t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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))))))
82 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {{{x}}} V
83 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (t = {{{x}}} → ⟪t, ⟪a, y⟫⟫ = ⟪{{{x}}}, ⟪a, y⟫⟫)
8483eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (t = {{{x}}} → (⟪t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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}}}, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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))))))
8582, 84ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (t(t = {{{x}}} t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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}}}, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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)))))
86 elin 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{x}}}, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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}}}, ⟪a, y⟫⟫ Ins2k Sk ⟪{{{x}}}, ⟪a, y⟫⟫ Ins3k (({{}} ×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)))))
87 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 {x} V
8887, 68, 10otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{x}}}, ⟪a, y⟫⟫ Ins2k Sk ↔ ⟪{x}, y Sk )
89 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 x V
9089, 10elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{x}, y Skx y)
9188, 90bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{x}}}, ⟪a, y⟫⟫ Ins2k Skx y)
9287, 68, 10otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{x}}}, ⟪a, y⟫⟫ Ins3k (({{}} ×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}, a (({{}} ×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))))
9389, 68eqtfinrelk 4487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{x}, a (({{}} ×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))) ↔ a = Tfin x)
9492, 93bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{x}}}, ⟪a, y⟫⟫ Ins3k (({{}} ×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))) ↔ a = Tfin x)
9591, 94anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((⟪{{{x}}}, ⟪a, y⟫⟫ Ins2k Sk ⟪{{{x}}}, ⟪a, y⟫⟫ Ins3k (({{}} ×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 a = Tfin x))
9685, 86, 953bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t(t = {{{x}}} t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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 a = Tfin x))
9796exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (xt(t = {{{x}}} t, ⟪a, y⟫⟫ ( Ins2k SkIns3k (({{}} ×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(x y a = Tfin x))
9873, 81, 973bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪a, y (( Ins2k SkIns3k (({{}} ×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)))) “k 111c) ↔ x(x y a = Tfin x))
9968, 10opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{a}, {y}⟫ SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c) ↔ ⟪a, y (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))
100 df-rex 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (x y a = Tfin xx(x y a = Tfin x))
10198, 99, 1003bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{a}, {y}⟫ SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c) ↔ x y a = Tfin x)
10271, 101bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{a}}}, ⟪w, {y}⟫⟫ Ins2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c) ↔ x y a = Tfin x)
10370, 102bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((⟪{{{a}}}, ⟪w, {y}⟫⟫ Ins3k Sk ↔ ⟪{{{a}}}, ⟪w, {y}⟫⟫ Ins2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) ↔ (a wx y a = Tfin x))
104103notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (¬ (⟪{{{a}}}, ⟪w, {y}⟫⟫ Ins3k Sk ↔ ⟪{{{a}}}, ⟪w, {y}⟫⟫ Ins2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) ↔ ¬ (a wx y a = Tfin x))
10564, 65, 1043bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (t(t = {{{a}}} t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))) ↔ ¬ (a wx y a = Tfin x))
106105exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (at(t = {{{a}}} t, ⟪w, {y}⟫⟫ ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c))) ↔ a ¬ (a wx y a = Tfin x))
10752, 60, 1063bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪w, {y}⟫ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ↔ a ¬ (a wx y a = Tfin x))
108107notbii 287 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ ⟪w, {y}⟫ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ↔ ¬ a ¬ (a wx y a = Tfin x))
10951elcompl 3226 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪w, {y}⟫ ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ↔ ¬ ⟪w, {y}⟫ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c))
110 abeq2 2459 . . . . . . . . . . . . . . . . . . . . . . . . 25 (w = {a x y a = Tfin x} ↔ a(a wx y a = Tfin x))
111 alex 1572 . . . . . . . . . . . . . . . . . . . . . . . . 25 (a(a wx y a = Tfin x) ↔ ¬ a ¬ (a wx y a = Tfin x))
112110, 111bitri 240 . . . . . . . . . . . . . . . . . . . . . . . 24 (w = {a x y a = Tfin x} ↔ ¬ a ¬ (a wx y a = Tfin x))
113108, 109, 1123bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪w, {y}⟫ ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ↔ w = {a x y a = Tfin x})
11448, 50, 1133bitri 262 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{{{w}}}, ⟪z, {{y}}⟫⟫ Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ↔ w = {a x y a = Tfin x})
11547, 26, 3otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{{w}}}, ⟪z, {{y}}⟫⟫ Ins3k Sk ↔ ⟪{w}, z Sk )
11649, 26elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{w}, z Skw z)
117115, 116bitri 240 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{{{w}}}, ⟪z, {{y}}⟫⟫ Ins3k Skw z)
118114, 117anbi12i 678 . . . . . . . . . . . . . . . . . . . . 21 ((⟪{{{w}}}, ⟪z, {{y}}⟫⟫ Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ⟪{{{w}}}, ⟪z, {{y}}⟫⟫ Ins3k Sk ) ↔ (w = {a x y a = Tfin x} w z))
11945, 46, 1183bitri 262 . . . . . . . . . . . . . . . . . . . 20 (t(t = {{{w}}} t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )) ↔ (w = {a x y a = Tfin x} w z))
120119exbii 1582 . . . . . . . . . . . . . . . . . . 19 (wt(t = {{{w}}} t, ⟪z, {{y}}⟫⟫ ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk )) ↔ w(w = {a x y a = Tfin x} w z))
12133, 41, 1203bitri 262 . . . . . . . . . . . . . . . . . 18 (⟪z, {{y}}⟫ (( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c) ↔ w(w = {a x y a = Tfin x} w z))
12226, 3, 27otkelins3k 4257 . . . . . . . . . . . . . . . . . 18 (⟪{{z}}, ⟪{{y}}, {n}⟫⟫ Ins3k (( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c) ↔ ⟪z, {{y}}⟫ (( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))
123 df-clel 2349 . . . . . . . . . . . . . . . . . 18 ({a x y a = Tfin x} zw(w = {a x y a = Tfin x} w z))
124121, 122, 1233bitr4i 268 . . . . . . . . . . . . . . . . 17 (⟪{{z}}, ⟪{{y}}, {n}⟫⟫ Ins3k (( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c) ↔ {a x y a = Tfin x} z)
12531, 124anbi12i 678 . . . . . . . . . . . . . . . 16 ((⟪{{z}}, ⟪{{y}}, {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))) ⟪{{z}}, ⟪{{y}}, {n}⟫⟫ Ins3k (( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) ↔ (z = Tfin n {a x y a = Tfin x} z))
12624, 25, 1253bitri 262 . . . . . . . . . . . . . . 15 (t(t = {{z}} t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ (z = Tfin n {a x y a = Tfin x} z))
127126exbii 1582 . . . . . . . . . . . . . 14 (zt(t = {{z}} t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ z(z = Tfin n {a x y a = Tfin x} z))
128 opkex 4114 . . . . . . . . . . . . . . . 16 ⟪{{y}}, {n}⟫ V
129128elimak 4260 . . . . . . . . . . . . . . 15 (⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c) ↔ t 1 1ct, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)))
130 elpw11c 4148 . . . . . . . . . . . . . . . . . . 19 (t 11cz t = {{z}})
131130anbi1i 676 . . . . . . . . . . . . . . . . . 18 ((t 11c t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ (z t = {{z}} t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))))
132 19.41v 1901 . . . . . . . . . . . . . . . . . 18 (z(t = {{z}} t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ (z t = {{z}} t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))))
133131, 132bitr4i 243 . . . . . . . . . . . . . . . . 17 ((t 11c t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ z(t = {{z}} t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))))
134133exbii 1582 . . . . . . . . . . . . . . . 16 (t(t 11c t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ tz(t = {{z}} t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))))
135 df-rex 2621 . . . . . . . . . . . . . . . 16 (t 1 1ct, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) ↔ t(t 11c t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))))
136 excom 1741 . . . . . . . . . . . . . . . 16 (zt(t = {{z}} t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))) ↔ tz(t = {{z}} t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))))
137134, 135, 1363bitr4i 268 . . . . . . . . . . . . . . 15 (t 1 1ct, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) ↔ zt(t = {{z}} t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))))
138129, 137bitri 240 . . . . . . . . . . . . . 14 (⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c) ↔ zt(t = {{z}} t, ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c))))
139 tfinex 4486 . . . . . . . . . . . . . . 15 Tfin n V
140139clel3 2978 . . . . . . . . . . . . . 14 ({a x y a = Tfin x} Tfin nz(z = Tfin n {a x y a = Tfin x} z))
141127, 138, 1403bitr4i 268 . . . . . . . . . . . . 13 (⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c) ↔ {a x y a = Tfin x} Tfin n)
142141notbii 287 . . . . . . . . . . . 12 (¬ ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c) ↔ ¬ {a x y a = Tfin x} Tfin n)
14320, 142anbi12i 678 . . . . . . . . . . 11 ((⟪{{y}}, {n}⟫ SIk (1 Nn ×k V) ¬ ⟪{{y}}, {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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)) ↔ (y Nn ¬ {a x y a = Tfin x} Tfin n))
144 annim 414 . . . . . . . . . . 11 ((y Nn ¬ {a x y a = Tfin x} Tfin n) ↔ ¬ (y Nn → {a x y a = Tfin x} Tfin n))
14513, 143, 1443bitri 262 . . . . . . . . . 10 (⟪{{y}}, {n}⟫ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)) ↔ ¬ (y Nn → {a x y a = Tfin x} Tfin n))
14612, 145anbi12i 678 . . . . . . . . 9 ((⟪{{y}}, {n}⟫ SIk Sk ⟪{{y}}, {n}⟫ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) ↔ (y n ¬ (y Nn → {a x y a = Tfin x} Tfin n)))
1476, 7, 1463bitri 262 . . . . . . . 8 (t(t = {{y}} t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))) ↔ (y n ¬ (y Nn → {a x y a = Tfin x} Tfin n)))
148147exbii 1582 . . . . . . 7 (yt(t = {{y}} t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))) ↔ y(y n ¬ (y Nn → {a x y a = Tfin x} Tfin n)))
14927elimak 4260 . . . . . . . 8 ({n} (( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) “k 11c) ↔ t 1 1ct, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))))
150 elpw11c 4148 . . . . . . . . . . . 12 (t 11cy t = {{y}})
151150anbi1i 676 . . . . . . . . . . 11 ((t 11c t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))) ↔ (y t = {{y}} t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))))
152 19.41v 1901 . . . . . . . . . . 11 (y(t = {{y}} t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))) ↔ (y t = {{y}} t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))))
153151, 152bitr4i 243 . . . . . . . . . 10 ((t 11c t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))) ↔ y(t = {{y}} t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))))
154153exbii 1582 . . . . . . . . 9 (t(t 11c t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))) ↔ ty(t = {{y}} t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))))
155 df-rex 2621 . . . . . . . . 9 (t 1 1ct, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) ↔ t(t 11c t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))))
156 excom 1741 . . . . . . . . 9 (yt(t = {{y}} t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))) ↔ ty(t = {{y}} t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))))
157154, 155, 1563bitr4i 268 . . . . . . . 8 (t 1 1ct, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) ↔ yt(t = {{y}} t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))))
158149, 157bitri 240 . . . . . . 7 ({n} (( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) “k 11c) ↔ yt(t = {{y}} t, {n}⟫ ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)))))
159 df-rex 2621 . . . . . . 7 (y n ¬ (y Nn → {a x y a = Tfin x} Tfin n) ↔ y(y n ¬ (y Nn → {a x y a = Tfin x} Tfin n)))
160148, 158, 1593bitr4i 268 . . . . . 6 ({n} (( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) “k 11c) ↔ y n ¬ (y Nn → {a x y a = Tfin x} Tfin n))
161160notbii 287 . . . . 5 (¬ {n} (( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) “k 11c) ↔ ¬ y n ¬ (y Nn → {a x y a = Tfin x} Tfin n))
16227elcompl 3226 . . . . 5 ({n} ∼ (( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) “k 11c) ↔ ¬ {n} (( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) “k 11c))
163 dfral2 2627 . . . . 5 (y n (y Nn → {a x y a = Tfin x} Tfin n) ↔ ¬ y n ¬ (y Nn → {a x y a = Tfin x} Tfin n))
164161, 162, 1633bitr4i 268 . . . 4 ({n} ∼ (( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) “k 11c) ↔ y n (y Nn → {a x y a = Tfin x} Tfin n))
1652, 164bitri 240 . . 3 (n 1 ∼ (( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) “k 11c) ↔ y n (y Nn → {a x y a = Tfin x} Tfin n))
166165abbi2i 2465 . 2 1 ∼ (( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) “k 11c) = {n y n (y Nn → {a x y a = Tfin x} Tfin n)}
167 ssetkex 4295 . . . . . . 7 Sk V
168167sikex 4298 . . . . . 6 SIk Sk V
169 nncex 4397 . . . . . . . . . . 11 Nn V
170169pwex 4330 . . . . . . . . . 10 Nn V
171170pw1ex 4304 . . . . . . . . 9 1 Nn V
172 vvex 4110 . . . . . . . . 9 V V
173171, 172xpkex 4290 . . . . . . . 8 (1 Nn ×k V) V
174173sikex 4298 . . . . . . 7 SIk (1 Nn ×k V) V
175 tfinrelkex 4488 . . . . . . . . . . 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
176175cnvkex 4288 . . . . . . . . . 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
177176ins2kex 4308 . . . . . . . . 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
178167ins3kex 4309 . . . . . . . . . . . . . . . . 17 Ins3k Sk V
179167ins2kex 4308 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Sk V
180175ins3kex 4309 . . . . . . . . . . . . . . . . . . . . 21 Ins3k (({{}} ×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
181179, 180inex 4106 . . . . . . . . . . . . . . . . . . . 20 ( Ins2k SkIns3k (({{}} ×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
182 1cex 4143 . . . . . . . . . . . . . . . . . . . . . 22 1c V
183182pw1ex 4304 . . . . . . . . . . . . . . . . . . . . 21 11c V
184183pw1ex 4304 . . . . . . . . . . . . . . . . . . . 20 111c V
185181, 184imakex 4301 . . . . . . . . . . . . . . . . . . 19 (( Ins2k SkIns3k (({{}} ×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)))) “k 111c) V
186185sikex 4298 . . . . . . . . . . . . . . . . . 18 SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c) V
187186ins2kex 4308 . . . . . . . . . . . . . . . . 17 Ins2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c) V
188178, 187symdifex 4109 . . . . . . . . . . . . . . . 16 ( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) V
189188, 184imakex 4301 . . . . . . . . . . . . . . 15 (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) V
190189complex 4105 . . . . . . . . . . . . . 14 ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) V
191190sikex 4298 . . . . . . . . . . . . 13 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) V
192191ins2kex 4308 . . . . . . . . . . . 12 Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) V
193192, 178inex 4106 . . . . . . . . . . 11 ( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) V
194193, 184imakex 4301 . . . . . . . . . 10 (( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c) V
195194ins3kex 4309 . . . . . . . . 9 Ins3k (( Ins2k SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c) V
196177, 195inex 4106 . . . . . . . 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) V
197196, 183imakex 4301 . . . . . . 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c) V
198174, 197difex 4108 . . . . . 6 ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c)) V
199168, 198inex 4106 . . . . 5 ( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) V
200199, 183imakex 4301 . . . 4 (( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) “k 11c) V
201200complex 4105 . . 3 ∼ (( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) “k 11c) V
202201uni1ex 4294 . 2 1 ∼ (( SIk Sk ∩ ( SIk (1 Nn ×k V) (( 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 SIk ∼ (( Ins3k SkIns2k SIk (( Ins2k SkIns3k (({{}} ×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)))) “k 111c)) “k 111c) ∩ Ins3k Sk ) “k 111c)) “k 11c))) “k 11c) V
203166, 202eqeltrri 2424 1 {n y n (y Nn → {a x y a = Tfin x} Tfin n)} V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wa 358  wal 1540  wex 1541   = wceq 1642   wcel 1710  {cab 2339  wral 2615  wrex 2616  Vcvv 2860  ccompl 3206   cdif 3207  cun 3208  cin 3209  csymdif 3210   wss 3258  c0 3551  cpw 3723  {csn 3738  copk 4058  1cuni1 4134  1cc1c 4135  1cpw1 4136   ×k cxpk 4175  kccnvk 4176   Ins2k cins2k 4177   Ins3k cins3k 4178  k cimak 4180   SIk csik 4182   Sk cssetk 4184   Ik cidk 4185   Nn cnnc 4374   Tfin ctfin 4436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-iota 4340  df-addc 4379  df-nnc 4380  df-tfin 4444
This theorem is referenced by:  tfinnn  4535
  Copyright terms: Public domain W3C validator