Metamath Proof Explorer

Theorem finixpnum

Description: A finite Cartesian product of numerable sets is numerable. (Contributed by Brendan Leahy, 24-Feb-2019)

Ref Expression
Assertion finixpnum 
|- ( ( A e. Fin /\ A. x e. A B e. dom card ) -> X_ x e. A B e. dom card )

Proof

Step Hyp Ref Expression
1 raleq 
 |-  ( w = (/) -> ( A. x e. w B e. dom card <-> A. x e. (/) B e. dom card ) )
2 ixpeq1 
 |-  ( w = (/) -> X_ x e. w B = X_ x e. (/) B )
3 ixp0x 
 |-  X_ x e. (/) B = { (/) }
4 2 3 eqtrdi 
 |-  ( w = (/) -> X_ x e. w B = { (/) } )
5 4 eleq1d 
 |-  ( w = (/) -> ( X_ x e. w B e. dom card <-> { (/) } e. dom card ) )
6 1 5 imbi12d 
 |-  ( w = (/) -> ( ( A. x e. w B e. dom card -> X_ x e. w B e. dom card ) <-> ( A. x e. (/) B e. dom card -> { (/) } e. dom card ) ) )
7 raleq 
 |-  ( w = y -> ( A. x e. w B e. dom card <-> A. x e. y B e. dom card ) )
8 ixpeq1 
 |-  ( w = y -> X_ x e. w B = X_ x e. y B )
9 8 eleq1d 
 |-  ( w = y -> ( X_ x e. w B e. dom card <-> X_ x e. y B e. dom card ) )
10 7 9 imbi12d 
 |-  ( w = y -> ( ( A. x e. w B e. dom card -> X_ x e. w B e. dom card ) <-> ( A. x e. y B e. dom card -> X_ x e. y B e. dom card ) ) )
11 raleq 
 |-  ( w = ( y u. { z } ) -> ( A. x e. w B e. dom card <-> A. x e. ( y u. { z } ) B e. dom card ) )
12 ralunb 
 |-  ( A. x e. ( y u. { z } ) B e. dom card <-> ( A. x e. y B e. dom card /\ A. x e. { z } B e. dom card ) )
13 vex 
 |-  z e. _V
14 ralsnsg 
 |-  ( z e. _V -> ( A. x e. { z } B e. dom card <-> [. z / x ]. B e. dom card ) )
15 sbcel1g 
 |-  ( z e. _V -> ( [. z / x ]. B e. dom card <-> [_ z / x ]_ B e. dom card ) )
16 14 15 bitrd 
 |-  ( z e. _V -> ( A. x e. { z } B e. dom card <-> [_ z / x ]_ B e. dom card ) )
17 13 16 ax-mp 
 |-  ( A. x e. { z } B e. dom card <-> [_ z / x ]_ B e. dom card )
18 17 anbi2i 
 |-  ( ( A. x e. y B e. dom card /\ A. x e. { z } B e. dom card ) <-> ( A. x e. y B e. dom card /\ [_ z / x ]_ B e. dom card ) )
19 12 18 bitri 
 |-  ( A. x e. ( y u. { z } ) B e. dom card <-> ( A. x e. y B e. dom card /\ [_ z / x ]_ B e. dom card ) )
20 11 19 bitrdi 
 |-  ( w = ( y u. { z } ) -> ( A. x e. w B e. dom card <-> ( A. x e. y B e. dom card /\ [_ z / x ]_ B e. dom card ) ) )
21 ixpeq1 
 |-  ( w = ( y u. { z } ) -> X_ x e. w B = X_ x e. ( y u. { z } ) B )
22 21 eleq1d 
 |-  ( w = ( y u. { z } ) -> ( X_ x e. w B e. dom card <-> X_ x e. ( y u. { z } ) B e. dom card ) )
23 20 22 imbi12d 
 |-  ( w = ( y u. { z } ) -> ( ( A. x e. w B e. dom card -> X_ x e. w B e. dom card ) <-> ( ( A. x e. y B e. dom card /\ [_ z / x ]_ B e. dom card ) -> X_ x e. ( y u. { z } ) B e. dom card ) ) )
24 raleq 
 |-  ( w = A -> ( A. x e. w B e. dom card <-> A. x e. A B e. dom card ) )
25 ixpeq1 
 |-  ( w = A -> X_ x e. w B = X_ x e. A B )
26 25 eleq1d 
 |-  ( w = A -> ( X_ x e. w B e. dom card <-> X_ x e. A B e. dom card ) )
27 24 26 imbi12d 
 |-  ( w = A -> ( ( A. x e. w B e. dom card -> X_ x e. w B e. dom card ) <-> ( A. x e. A B e. dom card -> X_ x e. A B e. dom card ) ) )
28 snfi 
 |-  { (/) } e. Fin
29 finnum 
 |-  ( { (/) } e. Fin -> { (/) } e. dom card )
30 28 29 mp1i 
 |-  ( A. x e. (/) B e. dom card -> { (/) } e. dom card )
31 pm2.27 
 |-  ( A. x e. y B e. dom card -> ( ( A. x e. y B e. dom card -> X_ x e. y B e. dom card ) -> X_ x e. y B e. dom card ) )
32 xpnum 
 |-  ( ( X_ x e. y B e. dom card /\ [_ z / x ]_ B e. dom card ) -> ( X_ x e. y B X. [_ z / x ]_ B ) e. dom card )
33 32 ancoms 
 |-  ( ( [_ z / x ]_ B e. dom card /\ X_ x e. y B e. dom card ) -> ( X_ x e. y B X. [_ z / x ]_ B ) e. dom card )
34 xp1st 
 |-  ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) -> ( 1st ` w ) e. X_ x e. y B )
35 ixpfn 
 |-  ( ( 1st ` w ) e. X_ x e. y B -> ( 1st ` w ) Fn y )
36 34 35 syl 
 |-  ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) -> ( 1st ` w ) Fn y )
37 fvex 
 |-  ( 2nd ` w ) e. _V
38 13 37 fnsn 
 |-  { <. z , ( 2nd ` w ) >. } Fn { z }
39 36 38 jctir 
 |-  ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) -> ( ( 1st ` w ) Fn y /\ { <. z , ( 2nd ` w ) >. } Fn { z } ) )
40 disjsn 
 |-  ( ( y i^i { z } ) = (/) <-> -. z e. y )
41 40 biimpri 
 |-  ( -. z e. y -> ( y i^i { z } ) = (/) )
42 fnun 
 |-  ( ( ( ( 1st ` w ) Fn y /\ { <. z , ( 2nd ` w ) >. } Fn { z } ) /\ ( y i^i { z } ) = (/) ) -> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) Fn ( y u. { z } ) )
43 39 41 42 syl2anr 
 |-  ( ( -. z e. y /\ w e. ( X_ x e. y B X. [_ z / x ]_ B ) ) -> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) Fn ( y u. { z } ) )
44 fvex 
 |-  ( 1st ` w ) e. _V
45 44 elixp 
 |-  ( ( 1st ` w ) e. X_ x e. y B <-> ( ( 1st ` w ) Fn y /\ A. x e. y ( ( 1st ` w ) ` x ) e. B ) )
46 34 45 sylib 
 |-  ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) -> ( ( 1st ` w ) Fn y /\ A. x e. y ( ( 1st ` w ) ` x ) e. B ) )
47 fvun1 
 |-  ( ( ( 1st ` w ) Fn y /\ { <. z , ( 2nd ` w ) >. } Fn { z } /\ ( ( y i^i { z } ) = (/) /\ x e. y ) ) -> ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) = ( ( 1st ` w ) ` x ) )
48 38 47 mp3an2 
 |-  ( ( ( 1st ` w ) Fn y /\ ( ( y i^i { z } ) = (/) /\ x e. y ) ) -> ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) = ( ( 1st ` w ) ` x ) )
49 48 anassrs 
 |-  ( ( ( ( 1st ` w ) Fn y /\ ( y i^i { z } ) = (/) ) /\ x e. y ) -> ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) = ( ( 1st ` w ) ` x ) )
50 49 eleq1d 
 |-  ( ( ( ( 1st ` w ) Fn y /\ ( y i^i { z } ) = (/) ) /\ x e. y ) -> ( ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B <-> ( ( 1st ` w ) ` x ) e. B ) )
51 50 biimprd 
 |-  ( ( ( ( 1st ` w ) Fn y /\ ( y i^i { z } ) = (/) ) /\ x e. y ) -> ( ( ( 1st ` w ) ` x ) e. B -> ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B ) )
52 51 ralimdva 
 |-  ( ( ( 1st ` w ) Fn y /\ ( y i^i { z } ) = (/) ) -> ( A. x e. y ( ( 1st ` w ) ` x ) e. B -> A. x e. y ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B ) )
53 52 ancoms 
 |-  ( ( ( y i^i { z } ) = (/) /\ ( 1st ` w ) Fn y ) -> ( A. x e. y ( ( 1st ` w ) ` x ) e. B -> A. x e. y ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B ) )
54 53 impr 
 |-  ( ( ( y i^i { z } ) = (/) /\ ( ( 1st ` w ) Fn y /\ A. x e. y ( ( 1st ` w ) ` x ) e. B ) ) -> A. x e. y ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B )
55 41 46 54 syl2an 
 |-  ( ( -. z e. y /\ w e. ( X_ x e. y B X. [_ z / x ]_ B ) ) -> A. x e. y ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B )
56 vsnid 
 |-  z e. { z }
57 41 56 jctir 
 |-  ( -. z e. y -> ( ( y i^i { z } ) = (/) /\ z e. { z } ) )
58 fvun2 
 |-  ( ( ( 1st ` w ) Fn y /\ { <. z , ( 2nd ` w ) >. } Fn { z } /\ ( ( y i^i { z } ) = (/) /\ z e. { z } ) ) -> ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` z ) = ( { <. z , ( 2nd ` w ) >. } ` z ) )
59 38 58 mp3an2 
 |-  ( ( ( 1st ` w ) Fn y /\ ( ( y i^i { z } ) = (/) /\ z e. { z } ) ) -> ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` z ) = ( { <. z , ( 2nd ` w ) >. } ` z ) )
60 36 57 59 syl2anr 
 |-  ( ( -. z e. y /\ w e. ( X_ x e. y B X. [_ z / x ]_ B ) ) -> ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` z ) = ( { <. z , ( 2nd ` w ) >. } ` z ) )
61 csbfv 
 |-  [_ z / x ]_ ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) = ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` z )
62 13 37 fvsn 
 |-  ( { <. z , ( 2nd ` w ) >. } ` z ) = ( 2nd ` w )
63 62 eqcomi 
 |-  ( 2nd ` w ) = ( { <. z , ( 2nd ` w ) >. } ` z )
64 60 61 63 3eqtr4g 
 |-  ( ( -. z e. y /\ w e. ( X_ x e. y B X. [_ z / x ]_ B ) ) -> [_ z / x ]_ ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) = ( 2nd ` w ) )
65 xp2nd 
 |-  ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) -> ( 2nd ` w ) e. [_ z / x ]_ B )
66 65 adantl 
 |-  ( ( -. z e. y /\ w e. ( X_ x e. y B X. [_ z / x ]_ B ) ) -> ( 2nd ` w ) e. [_ z / x ]_ B )
67 64 66 eqeltrd 
 |-  ( ( -. z e. y /\ w e. ( X_ x e. y B X. [_ z / x ]_ B ) ) -> [_ z / x ]_ ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. [_ z / x ]_ B )
68 ralsnsg 
 |-  ( z e. _V -> ( A. x e. { z } ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B <-> [. z / x ]. ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B ) )
69 13 68 ax-mp 
 |-  ( A. x e. { z } ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B <-> [. z / x ]. ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B )
70 sbcel12 
 |-  ( [. z / x ]. ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B <-> [_ z / x ]_ ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. [_ z / x ]_ B )
71 69 70 bitri 
 |-  ( A. x e. { z } ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B <-> [_ z / x ]_ ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. [_ z / x ]_ B )
72 67 71 sylibr 
 |-  ( ( -. z e. y /\ w e. ( X_ x e. y B X. [_ z / x ]_ B ) ) -> A. x e. { z } ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B )
73 ralun 
 |-  ( ( A. x e. y ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B /\ A. x e. { z } ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B ) -> A. x e. ( y u. { z } ) ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B )
74 55 72 73 syl2anc 
 |-  ( ( -. z e. y /\ w e. ( X_ x e. y B X. [_ z / x ]_ B ) ) -> A. x e. ( y u. { z } ) ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B )
75 snex 
 |-  { <. z , ( 2nd ` w ) >. } e. _V
76 44 75 unex 
 |-  ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) e. _V
77 76 elixp 
 |-  ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) e. X_ x e. ( y u. { z } ) B <-> ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ` x ) e. B ) )
78 43 74 77 sylanbrc 
 |-  ( ( -. z e. y /\ w e. ( X_ x e. y B X. [_ z / x ]_ B ) ) -> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) e. X_ x e. ( y u. { z } ) B )
79 78 fmpttd 
 |-  ( -. z e. y -> ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) : ( X_ x e. y B X. [_ z / x ]_ B ) --> X_ x e. ( y u. { z } ) B )
80 ixpfn 
 |-  ( u e. X_ x e. ( y u. { z } ) B -> u Fn ( y u. { z } ) )
81 ssun1 
 |-  y C_ ( y u. { z } )
82 fnssres 
 |-  ( ( u Fn ( y u. { z } ) /\ y C_ ( y u. { z } ) ) -> ( u |` y ) Fn y )
83 80 81 82 sylancl 
 |-  ( u e. X_ x e. ( y u. { z } ) B -> ( u |` y ) Fn y )
84 vex 
 |-  u e. _V
85 84 elixp 
 |-  ( u e. X_ x e. ( y u. { z } ) B <-> ( u Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( u ` x ) e. B ) )
86 ssralv 
 |-  ( y C_ ( y u. { z } ) -> ( A. x e. ( y u. { z } ) ( u ` x ) e. B -> A. x e. y ( u ` x ) e. B ) )
87 81 86 ax-mp 
 |-  ( A. x e. ( y u. { z } ) ( u ` x ) e. B -> A. x e. y ( u ` x ) e. B )
88 fvres 
 |-  ( x e. y -> ( ( u |` y ) ` x ) = ( u ` x ) )
89 88 eleq1d 
 |-  ( x e. y -> ( ( ( u |` y ) ` x ) e. B <-> ( u ` x ) e. B ) )
90 89 biimprd 
 |-  ( x e. y -> ( ( u ` x ) e. B -> ( ( u |` y ) ` x ) e. B ) )
91 90 ralimia 
 |-  ( A. x e. y ( u ` x ) e. B -> A. x e. y ( ( u |` y ) ` x ) e. B )
92 87 91 syl 
 |-  ( A. x e. ( y u. { z } ) ( u ` x ) e. B -> A. x e. y ( ( u |` y ) ` x ) e. B )
93 92 adantl 
 |-  ( ( u Fn ( y u. { z } ) /\ A. x e. ( y u. { z } ) ( u ` x ) e. B ) -> A. x e. y ( ( u |` y ) ` x ) e. B )
94 85 93 sylbi 
 |-  ( u e. X_ x e. ( y u. { z } ) B -> A. x e. y ( ( u |` y ) ` x ) e. B )
95 84 resex 
 |-  ( u |` y ) e. _V
96 95 elixp 
 |-  ( ( u |` y ) e. X_ x e. y B <-> ( ( u |` y ) Fn y /\ A. x e. y ( ( u |` y ) ` x ) e. B ) )
97 83 94 96 sylanbrc 
 |-  ( u e. X_ x e. ( y u. { z } ) B -> ( u |` y ) e. X_ x e. y B )
98 ssun2 
 |-  { z } C_ ( y u. { z } )
99 98 56 sselii 
 |-  z e. ( y u. { z } )
100 csbeq1 
 |-  ( w = z -> [_ w / x ]_ B = [_ z / x ]_ B )
101 100 fvixp 
 |-  ( ( u e. X_ w e. ( y u. { z } ) [_ w / x ]_ B /\ z e. ( y u. { z } ) ) -> ( u ` z ) e. [_ z / x ]_ B )
102 99 101 mpan2 
 |-  ( u e. X_ w e. ( y u. { z } ) [_ w / x ]_ B -> ( u ` z ) e. [_ z / x ]_ B )
103 nfcv 
 |-  F/_ w B
104 nfcsb1v 
 |-  F/_ x [_ w / x ]_ B
105 csbeq1a 
 |-  ( x = w -> B = [_ w / x ]_ B )
106 103 104 105 cbvixp 
 |-  X_ x e. ( y u. { z } ) B = X_ w e. ( y u. { z } ) [_ w / x ]_ B
107 102 106 eleq2s 
 |-  ( u e. X_ x e. ( y u. { z } ) B -> ( u ` z ) e. [_ z / x ]_ B )
108 opelxpi 
 |-  ( ( ( u |` y ) e. X_ x e. y B /\ ( u ` z ) e. [_ z / x ]_ B ) -> <. ( u |` y ) , ( u ` z ) >. e. ( X_ x e. y B X. [_ z / x ]_ B ) )
109 97 107 108 syl2anc 
 |-  ( u e. X_ x e. ( y u. { z } ) B -> <. ( u |` y ) , ( u ` z ) >. e. ( X_ x e. y B X. [_ z / x ]_ B ) )
110 109 adantl 
 |-  ( ( -. z e. y /\ u e. X_ x e. ( y u. { z } ) B ) -> <. ( u |` y ) , ( u ` z ) >. e. ( X_ x e. y B X. [_ z / x ]_ B ) )
111 disj3 
 |-  ( ( y i^i { z } ) = (/) <-> y = ( y \ { z } ) )
112 40 111 sylbb1 
 |-  ( -. z e. y -> y = ( y \ { z } ) )
113 difun2 
 |-  ( ( y u. { z } ) \ { z } ) = ( y \ { z } )
114 112 113 eqtr4di 
 |-  ( -. z e. y -> y = ( ( y u. { z } ) \ { z } ) )
115 114 reseq2d 
 |-  ( -. z e. y -> ( u |` y ) = ( u |` ( ( y u. { z } ) \ { z } ) ) )
116 115 uneq1d 
 |-  ( -. z e. y -> ( ( u |` y ) u. { <. z , ( u ` z ) >. } ) = ( ( u |` ( ( y u. { z } ) \ { z } ) ) u. { <. z , ( u ` z ) >. } ) )
117 116 adantr 
 |-  ( ( -. z e. y /\ u e. X_ x e. ( y u. { z } ) B ) -> ( ( u |` y ) u. { <. z , ( u ` z ) >. } ) = ( ( u |` ( ( y u. { z } ) \ { z } ) ) u. { <. z , ( u ` z ) >. } ) )
118 fvex 
 |-  ( u ` z ) e. _V
119 95 118 op1std 
 |-  ( w = <. ( u |` y ) , ( u ` z ) >. -> ( 1st ` w ) = ( u |` y ) )
120 95 118 op2ndd 
 |-  ( w = <. ( u |` y ) , ( u ` z ) >. -> ( 2nd ` w ) = ( u ` z ) )
121 120 opeq2d 
 |-  ( w = <. ( u |` y ) , ( u ` z ) >. -> <. z , ( 2nd ` w ) >. = <. z , ( u ` z ) >. )
122 121 sneqd 
 |-  ( w = <. ( u |` y ) , ( u ` z ) >. -> { <. z , ( 2nd ` w ) >. } = { <. z , ( u ` z ) >. } )
123 119 122 uneq12d 
 |-  ( w = <. ( u |` y ) , ( u ` z ) >. -> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) = ( ( u |` y ) u. { <. z , ( u ` z ) >. } ) )
124 eqid 
 |-  ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) = ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) )
125 snex 
 |-  { <. z , ( u ` z ) >. } e. _V
126 95 125 unex 
 |-  ( ( u |` y ) u. { <. z , ( u ` z ) >. } ) e. _V
127 123 124 126 fvmpt 
 |-  ( <. ( u |` y ) , ( u ` z ) >. e. ( X_ x e. y B X. [_ z / x ]_ B ) -> ( ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) ` <. ( u |` y ) , ( u ` z ) >. ) = ( ( u |` y ) u. { <. z , ( u ` z ) >. } ) )
128 109 127 syl 
 |-  ( u e. X_ x e. ( y u. { z } ) B -> ( ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) ` <. ( u |` y ) , ( u ` z ) >. ) = ( ( u |` y ) u. { <. z , ( u ` z ) >. } ) )
129 128 adantl 
 |-  ( ( -. z e. y /\ u e. X_ x e. ( y u. { z } ) B ) -> ( ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) ` <. ( u |` y ) , ( u ` z ) >. ) = ( ( u |` y ) u. { <. z , ( u ` z ) >. } ) )
130 fnsnsplit 
 |-  ( ( u Fn ( y u. { z } ) /\ z e. ( y u. { z } ) ) -> u = ( ( u |` ( ( y u. { z } ) \ { z } ) ) u. { <. z , ( u ` z ) >. } ) )
131 80 99 130 sylancl 
 |-  ( u e. X_ x e. ( y u. { z } ) B -> u = ( ( u |` ( ( y u. { z } ) \ { z } ) ) u. { <. z , ( u ` z ) >. } ) )
132 131 adantl 
 |-  ( ( -. z e. y /\ u e. X_ x e. ( y u. { z } ) B ) -> u = ( ( u |` ( ( y u. { z } ) \ { z } ) ) u. { <. z , ( u ` z ) >. } ) )
133 117 129 132 3eqtr4rd 
 |-  ( ( -. z e. y /\ u e. X_ x e. ( y u. { z } ) B ) -> u = ( ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) ` <. ( u |` y ) , ( u ` z ) >. ) )
134 fveq2 
 |-  ( v = <. ( u |` y ) , ( u ` z ) >. -> ( ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) ` v ) = ( ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) ` <. ( u |` y ) , ( u ` z ) >. ) )
135 134 rspceeqv 
 |-  ( ( <. ( u |` y ) , ( u ` z ) >. e. ( X_ x e. y B X. [_ z / x ]_ B ) /\ u = ( ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) ` <. ( u |` y ) , ( u ` z ) >. ) ) -> E. v e. ( X_ x e. y B X. [_ z / x ]_ B ) u = ( ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) ` v ) )
136 110 133 135 syl2anc 
 |-  ( ( -. z e. y /\ u e. X_ x e. ( y u. { z } ) B ) -> E. v e. ( X_ x e. y B X. [_ z / x ]_ B ) u = ( ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) ` v ) )
137 136 ralrimiva 
 |-  ( -. z e. y -> A. u e. X_ x e. ( y u. { z } ) B E. v e. ( X_ x e. y B X. [_ z / x ]_ B ) u = ( ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) ` v ) )
138 dffo3 
 |-  ( ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) : ( X_ x e. y B X. [_ z / x ]_ B ) -onto-> X_ x e. ( y u. { z } ) B <-> ( ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) : ( X_ x e. y B X. [_ z / x ]_ B ) --> X_ x e. ( y u. { z } ) B /\ A. u e. X_ x e. ( y u. { z } ) B E. v e. ( X_ x e. y B X. [_ z / x ]_ B ) u = ( ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) ` v ) ) )
139 79 137 138 sylanbrc 
 |-  ( -. z e. y -> ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) : ( X_ x e. y B X. [_ z / x ]_ B ) -onto-> X_ x e. ( y u. { z } ) B )
140 fonum 
 |-  ( ( ( X_ x e. y B X. [_ z / x ]_ B ) e. dom card /\ ( w e. ( X_ x e. y B X. [_ z / x ]_ B ) |-> ( ( 1st ` w ) u. { <. z , ( 2nd ` w ) >. } ) ) : ( X_ x e. y B X. [_ z / x ]_ B ) -onto-> X_ x e. ( y u. { z } ) B ) -> X_ x e. ( y u. { z } ) B e. dom card )
141 33 139 140 syl2anr 
 |-  ( ( -. z e. y /\ ( [_ z / x ]_ B e. dom card /\ X_ x e. y B e. dom card ) ) -> X_ x e. ( y u. { z } ) B e. dom card )
142 141 expr 
 |-  ( ( -. z e. y /\ [_ z / x ]_ B e. dom card ) -> ( X_ x e. y B e. dom card -> X_ x e. ( y u. { z } ) B e. dom card ) )
143 31 142 syl9r 
 |-  ( ( -. z e. y /\ [_ z / x ]_ B e. dom card ) -> ( A. x e. y B e. dom card -> ( ( A. x e. y B e. dom card -> X_ x e. y B e. dom card ) -> X_ x e. ( y u. { z } ) B e. dom card ) ) )
144 143 expimpd 
 |-  ( -. z e. y -> ( ( [_ z / x ]_ B e. dom card /\ A. x e. y B e. dom card ) -> ( ( A. x e. y B e. dom card -> X_ x e. y B e. dom card ) -> X_ x e. ( y u. { z } ) B e. dom card ) ) )
145 144 ancomsd 
 |-  ( -. z e. y -> ( ( A. x e. y B e. dom card /\ [_ z / x ]_ B e. dom card ) -> ( ( A. x e. y B e. dom card -> X_ x e. y B e. dom card ) -> X_ x e. ( y u. { z } ) B e. dom card ) ) )
146 145 com23 
 |-  ( -. z e. y -> ( ( A. x e. y B e. dom card -> X_ x e. y B e. dom card ) -> ( ( A. x e. y B e. dom card /\ [_ z / x ]_ B e. dom card ) -> X_ x e. ( y u. { z } ) B e. dom card ) ) )
147 146 adantl 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( A. x e. y B e. dom card -> X_ x e. y B e. dom card ) -> ( ( A. x e. y B e. dom card /\ [_ z / x ]_ B e. dom card ) -> X_ x e. ( y u. { z } ) B e. dom card ) ) )
148 6 10 23 27 30 147 findcard2s 
 |-  ( A e. Fin -> ( A. x e. A B e. dom card -> X_ x e. A B e. dom card ) )
149 148 imp 
 |-  ( ( A e. Fin /\ A. x e. A B e. dom card ) -> X_ x e. A B e. dom card )