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

Theorem eqtfinrelk 4486
 Description: Equality to a T raising expressed via a Kuratowski relationship. (Contributed by SF, 29-Jan-2015.)
Hypotheses
Ref Expression
eqtfinrelk.1 M V
eqtfinrelk.2 X V
Assertion
Ref Expression
eqtfinrelk (⟪{M}, X (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ X = Tfin M)

Proof of Theorem eqtfinrelk
Dummy variables n t y z x a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snex 4111 . . . . . . . . . 10 {} V
21snid 3760 . . . . . . . . 9 {} {{}}
3 eqtfinrelk.2 . . . . . . . . . 10 X V
41, 3opkelxpk 4248 . . . . . . . . 9 (⟪{}, X ({{}} ×k {}) ↔ ({} {{}} X {}))
52, 4mpbiran 884 . . . . . . . 8 (⟪{}, X ({{}} ×k {}) ↔ X {})
63elsnc 3756 . . . . . . . 8 (X {} ↔ X = )
75, 6bitri 240 . . . . . . 7 (⟪{}, X ({{}} ×k {}) ↔ X = )
87orbi1i 506 . . . . . 6 ((⟪{}, X ({{}} ×k {}) ⟪{}, X ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×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 ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))))
9 elun 3220 . . . . . 6 (⟪{}, X (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ (⟪{}, X ({{}} ×k {}) ⟪{}, X ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))))
101, 3opkelxpk 4248 . . . . . . . . . . 11 (⟪{}, X ({{}} ×k V) ↔ ({} {{}} X V))
112, 3, 10mpbir2an 886 . . . . . . . . . 10 ⟪{}, X ({{}} ×k V)
1211notnoti 115 . . . . . . . . 9 ¬ ¬ ⟪{}, X ({{}} ×k V)
1312intnan 880 . . . . . . . 8 ¬ (⟪{}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ¬ ⟪{}, X ({{}} ×k V))
14 eldif 3221 . . . . . . . 8 (⟪{}, X ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×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 ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ¬ ⟪{}, X ({{}} ×k V)))
1513, 14mtbir 290 . . . . . . 7 ¬ ⟪{}, X ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))
1615biorfi 396 . . . . . 6 (X = ↔ (X = ⟪{}, X ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))))
178, 9, 163bitr4i 268 . . . . 5 (⟪{}, X (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ X = )
1817a1i 10 . . . 4 (M = → (⟪{}, X (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ X = ))
19 sneq 3744 . . . . . 6 (M = → {M} = {})
2019opkeq1d 4065 . . . . 5 (M = → ⟪{M}, X⟫ = ⟪{}, X⟫)
2120eleq1d 2419 . . . 4 (M = → (⟪{M}, X (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ ⟪{}, X (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V)))))
22 iftrue 3668 . . . . 5 (M = → if(M = , , (℩y(y Nn a M 1a y))) = )
2322eqeq2d 2364 . . . 4 (M = → (X = if(M = , , (℩y(y Nn a M 1a y))) ↔ X = ))
2418, 21, 233bitr4d 276 . . 3 (M = → (⟪{M}, X (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ X = if(M = , , (℩y(y Nn a M 1a y)))))
25 iffalse 3669 . . . . 5 M = → if(M = , , (℩y(y Nn a M 1a y))) = (℩y(y Nn a M 1a y)))
2625eqeq2d 2364 . . . 4 M = → (X = if(M = , , (℩y(y Nn a M 1a y))) ↔ X = (℩y(y Nn a M 1a y))))
27 opkex 4113 . . . . . . . . 9 ⟪{M}, X V
2827elimak 4259 . . . . . . . 8 (⟪{M}, X (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ↔ t 1 11ct, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)))
29 elpw121c 4148 . . . . . . . . . . . 12 (t 111cz t = {{{z}}})
3029anbi1i 676 . . . . . . . . . . 11 ((t 111c t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))) ↔ (z t = {{{z}}} t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))))
31 19.41v 1901 . . . . . . . . . . 11 (z(t = {{{z}}} t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))) ↔ (z t = {{{z}}} t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))))
3230, 31bitr4i 243 . . . . . . . . . 10 ((t 111c t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))) ↔ z(t = {{{z}}} t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))))
3332exbii 1582 . . . . . . . . 9 (t(t 111c t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))) ↔ tz(t = {{{z}}} t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))))
34 df-rex 2620 . . . . . . . . 9 (t 1 11ct, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) ↔ t(t 111c t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))))
35 excom 1741 . . . . . . . . 9 (zt(t = {{{z}}} t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))) ↔ tz(t = {{{z}}} t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))))
3633, 34, 353bitr4i 268 . . . . . . . 8 (t 1 11ct, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) ↔ zt(t = {{{z}}} t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))))
37 snex 4111 . . . . . . . . . . 11 {{{z}}} V
38 opkeq1 4059 . . . . . . . . . . . 12 (t = {{{z}}} → ⟪t, ⟪{M}, X⟫⟫ = ⟪{{{z}}}, ⟪{M}, X⟫⟫)
3938eleq1d 2419 . . . . . . . . . . 11 (t = {{{z}}} → (⟪t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) ↔ ⟪{{{z}}}, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))))
4037, 39ceqsexv 2894 . . . . . . . . . 10 (t(t = {{{z}}} t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))) ↔ ⟪{{{z}}}, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)))
41 elsymdif 3223 . . . . . . . . . . 11 (⟪{{{z}}}, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) ↔ ¬ (⟪{{{z}}}, ⟪{M}, X⟫⟫ Ins2k Sk ↔ ⟪{{{z}}}, ⟪{M}, X⟫⟫ Ins3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)))
42 snex 4111 . . . . . . . . . . . . . 14 {z} V
43 snex 4111 . . . . . . . . . . . . . 14 {M} V
4442, 43, 3otkelins2k 4255 . . . . . . . . . . . . 13 (⟪{{{z}}}, ⟪{M}, X⟫⟫ Ins2k Sk ↔ ⟪{z}, X Sk )
45 vex 2862 . . . . . . . . . . . . . 14 z V
4645, 3elssetk 4270 . . . . . . . . . . . . 13 (⟪{z}, X Skz X)
4744, 46bitri 240 . . . . . . . . . . . 12 (⟪{{{z}}}, ⟪{M}, X⟫⟫ Ins2k Skz X)
48 snex 4111 . . . . . . . . . . . . . . . 16 {{n}} V
49 opkeq1 4059 . . . . . . . . . . . . . . . . 17 (t = {{n}} → ⟪t, ⟪{z}, {M}⟫⟫ = ⟪{{n}}, ⟪{z}, {M}⟫⟫)
5049eleq1d 2419 . . . . . . . . . . . . . . . 16 (t = {{n}} → (⟪t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) ↔ ⟪{{n}}, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))))
5148, 50ceqsexv 2894 . . . . . . . . . . . . . . 15 (t(t = {{n}} t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))) ↔ ⟪{{n}}, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)))
52 eldif 3221 . . . . . . . . . . . . . . 15 (⟪{{n}}, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) ↔ (⟪{{n}}, ⟪{z}, {M}⟫⟫ Ins3k k Sk ¬ ⟪{{n}}, ⟪{z}, {M}⟫⟫ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)))
53 vex 2862 . . . . . . . . . . . . . . . . . 18 n V
5453, 42, 43otkelins3k 4256 . . . . . . . . . . . . . . . . 17 (⟪{{n}}, ⟪{z}, {M}⟫⟫ Ins3k k Sk ↔ ⟪n, {z}⟫ k Sk )
5553, 42opkelcnvk 4250 . . . . . . . . . . . . . . . . 17 (⟪n, {z}⟫ k Sk ↔ ⟪{z}, n Sk )
5645, 53elssetk 4270 . . . . . . . . . . . . . . . . 17 (⟪{z}, n Skz n)
5754, 55, 563bitri 262 . . . . . . . . . . . . . . . 16 (⟪{{n}}, ⟪{z}, {M}⟫⟫ Ins3k k Skz n)
5853, 42, 43otkelins2k 4255 . . . . . . . . . . . . . . . . . 18 (⟪{{n}}, ⟪{z}, {M}⟫⟫ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c) ↔ ⟪n, {M}⟫ (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))
59 opkex 4113 . . . . . . . . . . . . . . . . . . . 20 n, {M}⟫ V
6059elimak 4259 . . . . . . . . . . . . . . . . . . 19 (⟪n, {M}⟫ (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c) ↔ t 1 1ct, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ))
61 elpw11c 4147 . . . . . . . . . . . . . . . . . . . . . . 23 (t 11cy t = {{y}})
6261anbi1i 676 . . . . . . . . . . . . . . . . . . . . . 22 ((t 11c t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )) ↔ (y t = {{y}} t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )))
63 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . 22 (y(t = {{y}} t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )) ↔ (y t = {{y}} t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )))
6462, 63bitr4i 243 . . . . . . . . . . . . . . . . . . . . 21 ((t 11c t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )) ↔ y(t = {{y}} t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )))
6564exbii 1582 . . . . . . . . . . . . . . . . . . . 20 (t(t 11c t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )) ↔ ty(t = {{y}} t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )))
66 df-rex 2620 . . . . . . . . . . . . . . . . . . . 20 (t 1 1ct, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) ↔ t(t 11c t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )))
67 excom 1741 . . . . . . . . . . . . . . . . . . . 20 (yt(t = {{y}} t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )) ↔ ty(t = {{y}} t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )))
6865, 66, 673bitr4i 268 . . . . . . . . . . . . . . . . . . 19 (t 1 1ct, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) ↔ yt(t = {{y}} t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )))
69 snex 4111 . . . . . . . . . . . . . . . . . . . . . 22 {{y}} V
70 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . 23 (t = {{y}} → ⟪t, ⟪n, {M}⟫⟫ = ⟪{{y}}, ⟪n, {M}⟫⟫)
7170eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . 22 (t = {{y}} → (⟪t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) ↔ ⟪{{y}}, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )))
7269, 71ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . 21 (t(t = {{y}} t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )) ↔ ⟪{{y}}, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ))
73 elsymdif 3223 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{{y}}, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) ↔ ¬ (⟪{{y}}, ⟪n, {M}⟫⟫ Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ ⟪{{y}}, ⟪n, {M}⟫⟫ Ins3k Ik ))
74 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . 25 y V
7574, 53, 43otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪{{y}}, ⟪n, {M}⟫⟫ Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ ⟪y, {M}⟫ (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))
76 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪y, {M}⟫ (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ (⟪y, {M}⟫ ( Nn ×k V) y, {M}⟫ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))
7774, 43opkelxpk 4248 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪y, {M}⟫ ( Nn ×k V) ↔ (y Nn {M} V))
7843, 77mpbiran2 885 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪y, {M}⟫ ( Nn ×k V) ↔ y Nn )
79 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 {{{{a}}}} V
80 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t = {{{{a}}}} → ⟪t, ⟪y, {M}⟫⟫ = ⟪{{{{a}}}}, ⟪y, {M}⟫⟫)
8180eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t = {{{{a}}}} → (⟪t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ↔ ⟪{{{{a}}}}, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))))
8279, 81ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t(t = {{{{a}}}} t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))) ↔ ⟪{{{{a}}}}, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)))
83 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪{{{{a}}}}, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ↔ (⟪{{{{a}}}}, ⟪y, {M}⟫⟫ Ins2k SIk Sk ⟪{{{{a}}}}, ⟪y, {M}⟫⟫ Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)))
84 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 {{a}} V
8584, 74, 43otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{{a}}}}, ⟪y, {M}⟫⟫ Ins2k SIk Sk ↔ ⟪{{a}}, {M}⟫ SIk Sk )
86 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 {a} V
87 eqtfinrelk.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 M V
8886, 87opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{a}}, {M}⟫ SIk Sk ↔ ⟪{a}, M Sk )
89 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 a V
9089, 87elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{a}, M Ska M)
9185, 88, 903bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟪{{{{a}}}}, ⟪y, {M}⟫⟫ Ins2k SIk Ska M)
92 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⟪{{a}}, y V
9392elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{a}}, y (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ↔ t 1 11ct, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ))
94 elpw121c 4148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (t 111cx t = {{{x}}})
9594anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((t 111c t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ (x t = {{{x}}} t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
96 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (x(t = {{{x}}} t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ (x t = {{{x}}} t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
9795, 96bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((t 111c t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ x(t = {{{x}}} t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
9897exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (t(t 111c t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ tx(t = {{{x}}} t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
99 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (t 1 11ct, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ t(t 111c t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
100 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (xt(t = {{{x}}} t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ tx(t = {{{x}}} t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
10198, 99, 1003bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t 1 11ct, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ xt(t = {{{x}}} t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
102 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {{{x}}} V
103 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (t = {{{x}}} → ⟪t, ⟪{{a}}, y⟫⟫ = ⟪{{{x}}}, ⟪{{a}}, y⟫⟫)
104103eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t = {{{x}}} → (⟪t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ ⟪{{{x}}}, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )))
105102, 104ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (t(t = {{{x}}} t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ ⟪{{{x}}}, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ))
106 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪{{{x}}}, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) ↔ (⟪{{{x}}}, ⟪{{a}}, y⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ⟪{{{x}}}, ⟪{{a}}, y⟫⟫ Ins2k Sk ))
107 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {x} V
108107, 84, 74otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{x}}}, ⟪{{a}}, y⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ ⟪{x}, {{a}}⟫ SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)))
109 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 x V
110109, 86opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{x}, {{a}}⟫ SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ ⟪x, {a}⟫ ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)))
111109, 89eqpw1relk 4479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪x, {a}⟫ ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ x = 1a)
112108, 110, 1113bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{x}}}, ⟪{{a}}, y⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ x = 1a)
113107, 84, 74otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{x}}}, ⟪{{a}}, y⟫⟫ Ins2k Sk ↔ ⟪{x}, y Sk )
114109, 74elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{x}, y Skx y)
115113, 114bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{x}}}, ⟪{{a}}, y⟫⟫ Ins2k Skx y)
116112, 115anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((⟪{{{x}}}, ⟪{{a}}, y⟫⟫ Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ⟪{{{x}}}, ⟪{{a}}, y⟫⟫ Ins2k Sk ) ↔ (x = 1a x y))
117105, 106, 1163bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (t(t = {{{x}}} t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ (x = 1a x y))
118117exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (xt(t = {{{x}}} t, ⟪{{a}}, y⟫⟫ ( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk )) ↔ x(x = 1a x y))
11993, 101, 1183bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{a}}, y (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ↔ x(x = 1a x y))
12084, 74, 43otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{{a}}}}, ⟪y, {M}⟫⟫ Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ↔ ⟪{{a}}, y (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))
121 df-clel 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1a yx(x = 1a x y))
122119, 120, 1213bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟪{{{{a}}}}, ⟪y, {M}⟫⟫ Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ↔ 1a y)
12391, 122anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((⟪{{{{a}}}}, ⟪y, {M}⟫⟫ Ins2k SIk Sk ⟪{{{{a}}}}, ⟪y, {M}⟫⟫ Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ↔ (a M 1a y))
12482, 83, 1233bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (t(t = {{{{a}}}} t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))) ↔ (a M 1a y))
125124exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (at(t = {{{{a}}}} t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))) ↔ a(a M 1a y))
126 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t 1 111ct, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ↔ t(t 1111c t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))))
127 elpw131c 4149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t 1111ca t = {{{{a}}}})
128127anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((t 1111c t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))) ↔ (a t = {{{{a}}}} t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))))
129 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (a(t = {{{{a}}}} t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))) ↔ (a t = {{{{a}}}} t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))))
130128, 129bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((t 1111c t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))) ↔ a(t = {{{{a}}}} t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))))
131130exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t(t 1111c t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))) ↔ ta(t = {{{{a}}}} t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))))
132126, 131bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (t 1 111ct, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) ↔ ta(t = {{{{a}}}} t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))))
133 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 y, {M}⟫ V
134133elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪y, {M}⟫ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c) ↔ t 1 111ct, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)))
135 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (at(t = {{{{a}}}} t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))) ↔ ta(t = {{{{a}}}} t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))))
136132, 134, 1353bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪y, {M}⟫ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c) ↔ at(t = {{{{a}}}} t, ⟪y, {M}⟫⟫ ( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c))))
137 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a M 1a ya(a M 1a y))
138125, 136, 1373bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪y, {M}⟫ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c) ↔ a M 1a y)
13978, 138anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟪y, {M}⟫ ( Nn ×k V) y, {M}⟫ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ (y Nn a M 1a y))
14075, 76, 1393bitri 262 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{y}}, ⟪n, {M}⟫⟫ Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ (y Nn a M 1a y))
14174, 53, 43otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪{{y}}, ⟪n, {M}⟫⟫ Ins3k Ik ↔ ⟪y, n Ik )
142 opkelidkg 4274 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((y V n V) → (⟪y, n Iky = n))
14374, 53, 142mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪y, n Iky = n)
144141, 143bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{y}}, ⟪n, {M}⟫⟫ Ins3k Iky = n)
145140, 144bibi12i 306 . . . . . . . . . . . . . . . . . . . . . 22 ((⟪{{y}}, ⟪n, {M}⟫⟫ Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ ⟪{{y}}, ⟪n, {M}⟫⟫ Ins3k Ik ) ↔ ((y Nn a M 1a y) ↔ y = n))
14673, 145xchbinx 301 . . . . . . . . . . . . . . . . . . . . 21 (⟪{{y}}, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) ↔ ¬ ((y Nn a M 1a y) ↔ y = n))
14772, 146bitri 240 . . . . . . . . . . . . . . . . . . . 20 (t(t = {{y}} t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )) ↔ ¬ ((y Nn a M 1a y) ↔ y = n))
148147exbii 1582 . . . . . . . . . . . . . . . . . . 19 (yt(t = {{y}} t, ⟪n, {M}⟫⟫ ( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik )) ↔ y ¬ ((y Nn a M 1a y) ↔ y = n))
14960, 68, 1483bitri 262 . . . . . . . . . . . . . . . . . 18 (⟪n, {M}⟫ (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c) ↔ y ¬ ((y Nn a M 1a y) ↔ y = n))
150 exnal 1574 . . . . . . . . . . . . . . . . . 18 (y ¬ ((y Nn a M 1a y) ↔ y = n) ↔ ¬ y((y Nn a M 1a y) ↔ y = n))
15158, 149, 1503bitrri 263 . . . . . . . . . . . . . . . . 17 y((y Nn a M 1a y) ↔ y = n) ↔ ⟪{{n}}, ⟪{z}, {M}⟫⟫ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))
152151con1bii 321 . . . . . . . . . . . . . . . 16 (¬ ⟪{{n}}, ⟪{z}, {M}⟫⟫ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c) ↔ y((y Nn a M 1a y) ↔ y = n))
15357, 152anbi12i 678 . . . . . . . . . . . . . . 15 ((⟪{{n}}, ⟪{z}, {M}⟫⟫ Ins3k k Sk ¬ ⟪{{n}}, ⟪{z}, {M}⟫⟫ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) ↔ (z n y((y Nn a M 1a y) ↔ y = n)))
15451, 52, 1533bitri 262 . . . . . . . . . . . . . 14 (t(t = {{n}} t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))) ↔ (z n y((y Nn a M 1a y) ↔ y = n)))
155154exbii 1582 . . . . . . . . . . . . 13 (nt(t = {{n}} t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))) ↔ n(z n y((y Nn a M 1a y) ↔ y = n)))
15642, 43, 3otkelins3k 4256 . . . . . . . . . . . . . 14 (⟪{{{z}}}, ⟪{M}, X⟫⟫ Ins3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c) ↔ ⟪{z}, {M}⟫ (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))
157 opkex 4113 . . . . . . . . . . . . . . 15 ⟪{z}, {M}⟫ V
158157elimak 4259 . . . . . . . . . . . . . 14 (⟪{z}, {M}⟫ (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c) ↔ t 1 1ct, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)))
159 elpw11c 4147 . . . . . . . . . . . . . . . . . 18 (t 11cn t = {{n}})
160159anbi1i 676 . . . . . . . . . . . . . . . . 17 ((t 11c t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))) ↔ (n t = {{n}} t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))))
161 19.41v 1901 . . . . . . . . . . . . . . . . 17 (n(t = {{n}} t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))) ↔ (n t = {{n}} t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))))
162160, 161bitr4i 243 . . . . . . . . . . . . . . . 16 ((t 11c t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))) ↔ n(t = {{n}} t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))))
163162exbii 1582 . . . . . . . . . . . . . . 15 (t(t 11c t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))) ↔ tn(t = {{n}} t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))))
164 df-rex 2620 . . . . . . . . . . . . . . 15 (t 1 1ct, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) ↔ t(t 11c t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))))
165 excom 1741 . . . . . . . . . . . . . . 15 (nt(t = {{n}} t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))) ↔ tn(t = {{n}} t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))))
166163, 164, 1653bitr4i 268 . . . . . . . . . . . . . 14 (t 1 1ct, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) ↔ nt(t = {{n}} t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))))
167156, 158, 1663bitri 262 . . . . . . . . . . . . 13 (⟪{{{z}}}, ⟪{M}, X⟫⟫ Ins3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c) ↔ nt(t = {{n}} t, ⟪{z}, {M}⟫⟫ ( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c))))
168 dfiota2 4340 . . . . . . . . . . . . . . 15 (℩y(y Nn a M 1a y)) = {n y((y Nn a M 1a y) ↔ y = n)}
169168eleq2i 2417 . . . . . . . . . . . . . 14 (z (℩y(y Nn a M 1a y)) ↔ z {n y((y Nn a M 1a y) ↔ y = n)})
170 eluniab 3903 . . . . . . . . . . . . . 14 (z {n y((y Nn a M 1a y) ↔ y = n)} ↔ n(z n y((y Nn a M 1a y) ↔ y = n)))
171169, 170bitri 240 . . . . . . . . . . . . 13 (z (℩y(y Nn a M 1a y)) ↔ n(z n y((y Nn a M 1a y) ↔ y = n)))
172155, 167, 1713bitr4i 268 . . . . . . . . . . . 12 (⟪{{{z}}}, ⟪{M}, X⟫⟫ Ins3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c) ↔ z (℩y(y Nn a M 1a y)))
17347, 172bibi12i 306 . . . . . . . . . . 11 ((⟪{{{z}}}, ⟪{M}, X⟫⟫ Ins2k Sk ↔ ⟪{{{z}}}, ⟪{M}, X⟫⟫ Ins3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) ↔ (z Xz (℩y(y Nn a M 1a y))))
17441, 173xchbinx 301 . . . . . . . . . 10 (⟪{{{z}}}, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) ↔ ¬ (z Xz (℩y(y Nn a M 1a y))))
17540, 174bitri 240 . . . . . . . . 9 (t(t = {{{z}}} t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))) ↔ ¬ (z Xz (℩y(y Nn a M 1a y))))
176175exbii 1582 . . . . . . . 8 (zt(t = {{{z}}} t, ⟪{M}, X⟫⟫ ( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c))) ↔ z ¬ (z Xz (℩y(y Nn a M 1a y))))
17728, 36, 1763bitri 262 . . . . . . 7 (⟪{M}, X (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ↔ z ¬ (z Xz (℩y(y Nn a M 1a y))))
178177notbii 287 . . . . . 6 (¬ ⟪{M}, X (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ↔ ¬ z ¬ (z Xz (℩y(y Nn a M 1a y))))
17927elcompl 3225 . . . . . 6 (⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ↔ ¬ ⟪{M}, X (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c))
180 dfcleq 2347 . . . . . . 7 (X = (℩y(y Nn a M 1a y)) ↔ z(z Xz (℩y(y Nn a M 1a y))))
181 alex 1572 . . . . . . 7 (z(z Xz (℩y(y Nn a M 1a y))) ↔ ¬ z ¬ (z Xz (℩y(y Nn a M 1a y))))
182180, 181bitri 240 . . . . . 6 (X = (℩y(y Nn a M 1a y)) ↔ ¬ z ¬ (z Xz (℩y(y Nn a M 1a y))))
183178, 179, 1823bitr4i 268 . . . . 5 (⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ↔ X = (℩y(y Nn a M 1a y)))
184183a1i 10 . . . 4 M = → (⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ↔ X = (℩y(y Nn a M 1a y))))
18543, 3opkelxpk 4248 . . . . . . . . . . 11 (⟪{M}, X ({{}} ×k V) ↔ ({M} {{}} X V))
1863biantru 491 . . . . . . . . . . 11 ({M} {{}} ↔ ({M} {{}} X V))
18743elsnc 3756 . . . . . . . . . . . 12 ({M} {{}} ↔ {M} = {})
18887sneqb 3876 . . . . . . . . . . . 12 ({M} = {} ↔ M = )
189187, 188bitri 240 . . . . . . . . . . 11 ({M} {{}} ↔ M = )
190185, 186, 1893bitr2i 264 . . . . . . . . . 10 (⟪{M}, X ({{}} ×k V) ↔ M = )
191190biimpi 186 . . . . . . . . 9 (⟪{M}, X ({{}} ×k V) → M = )
192191con3i 127 . . . . . . . 8 M = → ¬ ⟪{M}, X ({{}} ×k V))
193192biantrud 493 . . . . . . 7 M = → (⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ↔ (⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ¬ ⟪{M}, X ({{}} ×k V))))
194 simpl 443 . . . . . . . . 9 ((M = X = ) → M = )
195194con3i 127 . . . . . . . 8 M = → ¬ (M = X = ))
196 biorf 394 . . . . . . . 8 (¬ (M = X = ) → ((⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ¬ ⟪{M}, X ({{}} ×k V)) ↔ ((M = X = ) (⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ¬ ⟪{M}, X ({{}} ×k V)))))
197195, 196syl 15 . . . . . . 7 M = → ((⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ¬ ⟪{M}, X ({{}} ×k V)) ↔ ((M = X = ) (⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ¬ ⟪{M}, X ({{}} ×k V)))))
198193, 197bitrd 244 . . . . . 6 M = → (⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ↔ ((M = X = ) (⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ¬ ⟪{M}, X ({{}} ×k V)))))
19943, 3opkelxpk 4248 . . . . . . . 8 (⟪{M}, X ({{}} ×k {}) ↔ ({M} {{}} X {}))
200189, 6anbi12i 678 . . . . . . . 8 (({M} {{}} X {}) ↔ (M = X = ))
201199, 200bitri 240 . . . . . . 7 (⟪{M}, X ({{}} ×k {}) ↔ (M = X = ))
202 eldif 3221 . . . . . . 7 (⟪{M}, X ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V)) ↔ (⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ¬ ⟪{M}, X ({{}} ×k V)))
203201, 202orbi12i 507 . . . . . 6 ((⟪{M}, X ({{}} ×k {}) ⟪{M}, X ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ ((M = X = ) (⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ¬ ⟪{M}, X ({{}} ×k V))))
204198, 203syl6bbr 254 . . . . 5 M = → (⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ↔ (⟪{M}, X ({{}} ×k {}) ⟪{M}, X ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V)))))
205 elun 3220 . . . . 5 (⟪{M}, X (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ (⟪{M}, X ({{}} ×k {}) ⟪{M}, X ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))))
206204, 205syl6bbr 254 . . . 4 M = → (⟪{M}, X ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ↔ ⟪{M}, X (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V)))))
20726, 184, 2063bitr2rd 273 . . 3 M = → (⟪{M}, X (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ X = if(M = , , (℩y(y Nn a M 1a y)))))
20824, 207pm2.61i 156 . 2 (⟪{M}, X (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ X = if(M = , , (℩y(y Nn a M 1a y))))
209 df-tfin 4443 . . 3 Tfin M = if(M = , , (℩y(y Nn a M 1a y)))
210209eqeq2i 2363 . 2 (X = Tfin MX = if(M = , , (℩y(y Nn a M 1a y))))
211208, 210bitr4i 243 1 (⟪{M}, X (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ X = Tfin M)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 176   ∨ wo 357   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  ∃wrex 2615  Vcvv 2859   ∼ ccompl 3205   ∖ cdif 3206   ∪ cun 3207   ∩ cin 3208   ⊕ csymdif 3209  ∅c0 3550   ifcif 3662  ℘cpw 3722  {csn 3737  ∪cuni 3891  ⟪copk 4057  1cc1c 4134  ℘1cpw1 4135   ×k cxpk 4174  ◡kccnvk 4175   Ins2k cins2k 4176   Ins3k cins3k 4177   “k cimak 4179   SIk csik 4181   Sk cssetk 4183   Ik cidk 4184  ℩cio 4337   Nn cnnc 4373   Tfin ctfin 4435 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-sn 4087 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-opk 4058  df-1c 4136  df-pw1 4137  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-sik 4192  df-ssetk 4193  df-idk 4195  df-iota 4339  df-tfin 4443 This theorem is referenced by:  sfintfinlem1  4531  tfinnnlem1  4533  vfinspss  4551  vfinspclt  4552  vfinncsp  4554
 Copyright terms: Public domain W3C validator