Metamath Proof Explorer

Theorem marypha1lem

Description: Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015)

Ref Expression
Assertion marypha1lem ⊢A∈Fin→b∈Fin→∀c∈𝒫A×b∀d∈𝒫Ad≼cd→∃e∈𝒫ce:A⟶1-1V

Proof

Step Hyp Ref Expression
1 xpeq1 ⊢a=f→a×b=f×b
2 1 pweqd ⊢a=f→𝒫a×b=𝒫f×b
3 pweq ⊢a=f→𝒫a=𝒫f
4 3 raleqdv ⊢a=f→∀d∈𝒫ad≼cd↔∀d∈𝒫fd≼cd
5 f1eq2 ⊢a=f→e:a⟶1-1V↔e:f⟶1-1V
6 5 rexbidv ⊢a=f→∃e∈𝒫ce:a⟶1-1V↔∃e∈𝒫ce:f⟶1-1V
7 4 6 imbi12d ⊢a=f→∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔∀d∈𝒫fd≼cd→∃e∈𝒫ce:f⟶1-1V
8 2 7 raleqbidv ⊢a=f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔∀c∈𝒫f×b∀d∈𝒫fd≼cd→∃e∈𝒫ce:f⟶1-1V
9 8 imbi2d ⊢a=f→b∈Fin→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔b∈Fin→∀c∈𝒫f×b∀d∈𝒫fd≼cd→∃e∈𝒫ce:f⟶1-1V
10 xpeq1 ⊢a=A→a×b=A×b
11 10 pweqd ⊢a=A→𝒫a×b=𝒫A×b
12 pweq ⊢a=A→𝒫a=𝒫A
13 12 raleqdv ⊢a=A→∀d∈𝒫ad≼cd↔∀d∈𝒫Ad≼cd
14 f1eq2 ⊢a=A→e:a⟶1-1V↔e:A⟶1-1V
15 14 rexbidv ⊢a=A→∃e∈𝒫ce:a⟶1-1V↔∃e∈𝒫ce:A⟶1-1V
16 13 15 imbi12d ⊢a=A→∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔∀d∈𝒫Ad≼cd→∃e∈𝒫ce:A⟶1-1V
17 11 16 raleqbidv ⊢a=A→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔∀c∈𝒫A×b∀d∈𝒫Ad≼cd→∃e∈𝒫ce:A⟶1-1V
18 17 imbi2d ⊢a=A→b∈Fin→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔b∈Fin→∀c∈𝒫A×b∀d∈𝒫Ad≼cd→∃e∈𝒫ce:A⟶1-1V
19 bi2.04 ⊢a⊂f→b∈Fin→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔b∈Fin→a⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V
20 19 albii ⊢∀aa⊂f→b∈Fin→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔∀ab∈Fin→a⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V
21 19.21v ⊢∀ab∈Fin→a⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔b∈Fin→∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V
22 20 21 bitri ⊢∀aa⊂f→b∈Fin→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔b∈Fin→∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V
23 0elpw ⊢∅∈𝒫g
24 f10 ⊢∅:∅⟶1-1V
25 f1eq1 ⊢e=∅→e:∅⟶1-1V↔∅:∅⟶1-1V
26 25 rspcev ⊢∅∈𝒫g∧∅:∅⟶1-1V→∃e∈𝒫ge:∅⟶1-1V
27 23 24 26 mp2an ⊢∃e∈𝒫ge:∅⟶1-1V
28 f1eq2 ⊢f=∅→e:f⟶1-1V↔e:∅⟶1-1V
29 28 rexbidv ⊢f=∅→∃e∈𝒫ge:f⟶1-1V↔∃e∈𝒫ge:∅⟶1-1V
30 27 29 mpbiri ⊢f=∅→∃e∈𝒫ge:f⟶1-1V
31 30 a1i ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh→f=∅→∃e∈𝒫ge:f⟶1-1V
32 n0 ⊢f≠∅↔∃ii∈f
33 snelpwi ⊢i∈f→i∈𝒫f
34 id ⊢d=i→d=i
35 imaeq2 ⊢d=i→gd=gi
36 34 35 breq12d ⊢d=i→d≼gd↔i≼gi
37 36 rspcva ⊢i∈𝒫f∧∀d∈𝒫fd≼gd→i≼gi
38 vex ⊢i∈V
39 38 snnz ⊢i≠∅
40 vsnex ⊢i∈V
41 40 0sdom ⊢∅≺i↔i≠∅
42 39 41 mpbir ⊢∅≺i
43 sdomdomtr ⊢∅≺i∧i≼gi→∅≺gi
44 42 43 mpan ⊢i≼gi→∅≺gi
45 vex ⊢g∈V
46 45 imaex ⊢gi∈V
47 46 0sdom ⊢∅≺gi↔gi≠∅
48 44 47 sylib ⊢i≼gi→gi≠∅
49 37 48 syl ⊢i∈𝒫f∧∀d∈𝒫fd≼gd→gi≠∅
50 49 expcom ⊢∀d∈𝒫fd≼gd→i∈𝒫f→gi≠∅
51 33 50 syl5 ⊢∀d∈𝒫fd≼gd→i∈f→gi≠∅
52 51 adantl ⊢g∈𝒫f×b∧∀d∈𝒫fd≼gd→i∈f→gi≠∅
53 52 ad2antlr ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh→i∈f→gi≠∅
54 53 impr ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f→gi≠∅
55 n0 ⊢gi≠∅↔∃jj∈gi
56 54 55 sylib ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f→∃jj∈gi
57 45 imaex ⊢gc∈V
58 57 difexi ⊢gc∖j∈V
59 58 0dom ⊢∅≼gc∖j
60 breq1 ⊢c=∅→c≼gc∖j↔∅≼gc∖j
61 59 60 mpbiri ⊢c=∅→c≼gc∖j
62 61 a1i ⊢∀hh⊂f∧h≠∅→h≺gh∧i∈f∧c∈𝒫f∖i→c=∅→c≼gc∖j
63 simpll ⊢∀hh⊂f∧h≠∅→h≺gh∧i∈f∧c∈𝒫f∖i∧c≠∅→∀hh⊂f∧h≠∅→h≺gh
64 elpwi ⊢c∈𝒫f∖i→c⊆f∖i
65 64 ad2antrl ⊢∀hh⊂f∧h≠∅→h≺gh∧i∈f∧c∈𝒫f∖i∧c≠∅→c⊆f∖i
66 difsnpss ⊢i∈f↔f∖i⊂f
67 66 biimpi ⊢i∈f→f∖i⊂f
68 67 ad2antlr ⊢∀hh⊂f∧h≠∅→h≺gh∧i∈f∧c∈𝒫f∖i∧c≠∅→f∖i⊂f
69 65 68 sspsstrd ⊢∀hh⊂f∧h≠∅→h≺gh∧i∈f∧c∈𝒫f∖i∧c≠∅→c⊂f
70 simprr ⊢∀hh⊂f∧h≠∅→h≺gh∧i∈f∧c∈𝒫f∖i∧c≠∅→c≠∅
71 69 70 jca ⊢∀hh⊂f∧h≠∅→h≺gh∧i∈f∧c∈𝒫f∖i∧c≠∅→c⊂f∧c≠∅
72 psseq1 ⊢h=c→h⊂f↔c⊂f
73 neeq1 ⊢h=c→h≠∅↔c≠∅
74 72 73 anbi12d ⊢h=c→h⊂f∧h≠∅↔c⊂f∧c≠∅
75 id ⊢h=c→h=c
76 imaeq2 ⊢h=c→gh=gc
77 75 76 breq12d ⊢h=c→h≺gh↔c≺gc
78 74 77 imbi12d ⊢h=c→h⊂f∧h≠∅→h≺gh↔c⊂f∧c≠∅→c≺gc
79 78 spvv ⊢∀hh⊂f∧h≠∅→h≺gh→c⊂f∧c≠∅→c≺gc
80 63 71 79 sylc ⊢∀hh⊂f∧h≠∅→h≺gh∧i∈f∧c∈𝒫f∖i∧c≠∅→c≺gc
81 domdifsn ⊢c≺gc→c≼gc∖j
82 80 81 syl ⊢∀hh⊂f∧h≠∅→h≺gh∧i∈f∧c∈𝒫f∖i∧c≠∅→c≼gc∖j
83 82 expr ⊢∀hh⊂f∧h≠∅→h≺gh∧i∈f∧c∈𝒫f∖i→c≠∅→c≼gc∖j
84 62 83 pm2.61dne ⊢∀hh⊂f∧h≠∅→h≺gh∧i∈f∧c∈𝒫f∖i→c≼gc∖j
85 84 adantlrr ⊢∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi∧c∈𝒫f∖i→c≼gc∖j
86 85 adantll ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi∧c∈𝒫f∖i→c≼gc∖j
87 df-ss ⊢c⊆f∖i↔c∩f∖i=c
88 64 87 sylib ⊢c∈𝒫f∖i→c∩f∖i=c
89 88 imaeq2d ⊢c∈𝒫f∖i→gc∩f∖i=gc
90 89 ineq1d ⊢c∈𝒫f∖i→gc∩f∖i∩b∖j=gc∩b∖j
91 90 adantl ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi∧c∈𝒫f∖i→gc∩f∖i∩b∖j=gc∩b∖j
92 indif2 ⊢gc∩b∖j=gc∩b∖j
93 imassrn ⊢gc⊆ran⁡g
94 elpwi ⊢g∈𝒫f×b→g⊆f×b
95 rnss ⊢g⊆f×b→ran⁡g⊆ran⁡f×b
96 rnxpss ⊢ran⁡f×b⊆b
97 95 96 sstrdi ⊢g⊆f×b→ran⁡g⊆b
98 94 97 syl ⊢g∈𝒫f×b→ran⁡g⊆b
99 93 98 sstrid ⊢g∈𝒫f×b→gc⊆b
100 df-ss ⊢gc⊆b↔gc∩b=gc
101 99 100 sylib ⊢g∈𝒫f×b→gc∩b=gc
102 101 difeq1d ⊢g∈𝒫f×b→gc∩b∖j=gc∖j
103 102 ad2antrl ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd→gc∩b∖j=gc∖j
104 92 103 eqtrid ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd→gc∩b∖j=gc∖j
105 104 ad2antrr ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi∧c∈𝒫f∖i→gc∩b∖j=gc∖j
106 91 105 eqtrd ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi∧c∈𝒫f∖i→gc∩f∖i∩b∖j=gc∖j
107 86 106 breqtrrd ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi∧c∈𝒫f∖i→c≼gc∩f∖i∩b∖j
108 107 ralrimiva ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi→∀c∈𝒫f∖ic≼gc∩f∖i∩b∖j
109 id ⊢c=d→c=d
110 imainrect ⊢g∩f∖i×b∖jc=gc∩f∖i∩b∖j
111 imaeq2 ⊢c=d→g∩f∖i×b∖jc=g∩f∖i×b∖jd
112 110 111 eqtr3id ⊢c=d→gc∩f∖i∩b∖j=g∩f∖i×b∖jd
113 109 112 breq12d ⊢c=d→c≼gc∩f∖i∩b∖j↔d≼g∩f∖i×b∖jd
114 113 cbvralvw ⊢∀c∈𝒫f∖ic≼gc∩f∖i∩b∖j↔∀d∈𝒫f∖id≼g∩f∖i×b∖jd
115 108 114 sylib ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi→∀d∈𝒫f∖id≼g∩f∖i×b∖jd
116 115 adantllr ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi→∀d∈𝒫f∖id≼g∩f∖i×b∖jd
117 inss2 ⊢g∩f∖i×b∖j⊆f∖i×b∖j
118 difss ⊢b∖j⊆b
119 xpss2 ⊢b∖j⊆b→f∖i×b∖j⊆f∖i×b
120 118 119 ax-mp ⊢f∖i×b∖j⊆f∖i×b
121 117 120 sstri ⊢g∩f∖i×b∖j⊆f∖i×b
122 45 inex1 ⊢g∩f∖i×b∖j∈V
123 122 elpw ⊢g∩f∖i×b∖j∈𝒫f∖i×b↔g∩f∖i×b∖j⊆f∖i×b
124 121 123 mpbir ⊢g∩f∖i×b∖j∈𝒫f∖i×b
125 simpllr ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi→∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V
126 67 adantr ⊢i∈f∧j∈gi→f∖i⊂f
127 126 ad2antll ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi→f∖i⊂f
128 vex ⊢f∈V
129 128 difexi ⊢f∖i∈V
130 psseq1 ⊢a=f∖i→a⊂f↔f∖i⊂f
131 xpeq1 ⊢a=f∖i→a×b=f∖i×b
132 131 pweqd ⊢a=f∖i→𝒫a×b=𝒫f∖i×b
133 pweq ⊢a=f∖i→𝒫a=𝒫f∖i
134 133 raleqdv ⊢a=f∖i→∀d∈𝒫ad≼cd↔∀d∈𝒫f∖id≼cd
135 f1eq2 ⊢a=f∖i→e:a⟶1-1V↔e:f∖i⟶1-1V
136 135 rexbidv ⊢a=f∖i→∃e∈𝒫ce:a⟶1-1V↔∃e∈𝒫ce:f∖i⟶1-1V
137 134 136 imbi12d ⊢a=f∖i→∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔∀d∈𝒫f∖id≼cd→∃e∈𝒫ce:f∖i⟶1-1V
138 132 137 raleqbidv ⊢a=f∖i→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔∀c∈𝒫f∖i×b∀d∈𝒫f∖id≼cd→∃e∈𝒫ce:f∖i⟶1-1V
139 130 138 imbi12d ⊢a=f∖i→a⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔f∖i⊂f→∀c∈𝒫f∖i×b∀d∈𝒫f∖id≼cd→∃e∈𝒫ce:f∖i⟶1-1V
140 129 139 spcv ⊢∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V→f∖i⊂f→∀c∈𝒫f∖i×b∀d∈𝒫f∖id≼cd→∃e∈𝒫ce:f∖i⟶1-1V
141 125 127 140 sylc ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi→∀c∈𝒫f∖i×b∀d∈𝒫f∖id≼cd→∃e∈𝒫ce:f∖i⟶1-1V
142 imaeq1 ⊢c=g∩f∖i×b∖j→cd=g∩f∖i×b∖jd
143 142 breq2d ⊢c=g∩f∖i×b∖j→d≼cd↔d≼g∩f∖i×b∖jd
144 143 ralbidv ⊢c=g∩f∖i×b∖j→∀d∈𝒫f∖id≼cd↔∀d∈𝒫f∖id≼g∩f∖i×b∖jd
145 pweq ⊢c=g∩f∖i×b∖j→𝒫c=𝒫g∩f∖i×b∖j
146 145 rexeqdv ⊢c=g∩f∖i×b∖j→∃e∈𝒫ce:f∖i⟶1-1V↔∃e∈𝒫g∩f∖i×b∖je:f∖i⟶1-1V
147 144 146 imbi12d ⊢c=g∩f∖i×b∖j→∀d∈𝒫f∖id≼cd→∃e∈𝒫ce:f∖i⟶1-1V↔∀d∈𝒫f∖id≼g∩f∖i×b∖jd→∃e∈𝒫g∩f∖i×b∖je:f∖i⟶1-1V
148 147 rspcva ⊢g∩f∖i×b∖j∈𝒫f∖i×b∧∀c∈𝒫f∖i×b∀d∈𝒫f∖id≼cd→∃e∈𝒫ce:f∖i⟶1-1V→∀d∈𝒫f∖id≼g∩f∖i×b∖jd→∃e∈𝒫g∩f∖i×b∖je:f∖i⟶1-1V
149 124 141 148 sylancr ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi→∀d∈𝒫f∖id≼g∩f∖i×b∖jd→∃e∈𝒫g∩f∖i×b∖je:f∖i⟶1-1V
150 116 149 mpd ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi→∃e∈𝒫g∩f∖i×b∖je:f∖i⟶1-1V
151 f1eq1 ⊢e=k→e:f∖i⟶1-1V↔k:f∖i⟶1-1V
152 151 cbvrexvw ⊢∃e∈𝒫g∩f∖i×b∖je:f∖i⟶1-1V↔∃k∈𝒫g∩f∖i×b∖jk:f∖i⟶1-1V
153 150 152 sylib ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi→∃k∈𝒫g∩f∖i×b∖jk:f∖i⟶1-1V
154 vex ⊢j∈V
155 38 154 elimasn ⊢j∈gi↔ij∈g
156 155 biimpi ⊢j∈gi→ij∈g
157 156 snssd ⊢j∈gi→ij⊆g
158 157 ad2antlr ⊢i∈f∧j∈gi∧k∈𝒫g∩f∖i×b∖j→ij⊆g
159 elpwi ⊢k∈𝒫g∩f∖i×b∖j→k⊆g∩f∖i×b∖j
160 inss1 ⊢g∩f∖i×b∖j⊆g
161 159 160 sstrdi ⊢k∈𝒫g∩f∖i×b∖j→k⊆g
162 161 adantl ⊢i∈f∧j∈gi∧k∈𝒫g∩f∖i×b∖j→k⊆g
163 158 162 unssd ⊢i∈f∧j∈gi∧k∈𝒫g∩f∖i×b∖j→ij∪k⊆g
164 45 elpw2 ⊢ij∪k∈𝒫g↔ij∪k⊆g
165 163 164 sylibr ⊢i∈f∧j∈gi∧k∈𝒫g∩f∖i×b∖j→ij∪k∈𝒫g
166 165 ad2ant2lr ⊢g∈𝒫f×b∧i∈f∧j∈gi∧k∈𝒫g∩f∖i×b∖j∧k:f∖i⟶1-1V→ij∪k∈𝒫g
167 38 154 f1osn ⊢ij:i⟶1-1 ontoj
168 167 a1i ⊢k∈𝒫g∩f∖i×b∖j∧k:f∖i⟶1-1V→ij:i⟶1-1 ontoj
169 f1f1orn ⊢k:f∖i⟶1-1V→k:f∖i⟶1-1 ontoran⁡k
170 169 adantl ⊢k∈𝒫g∩f∖i×b∖j∧k:f∖i⟶1-1V→k:f∖i⟶1-1 ontoran⁡k
171 disjdif ⊢i∩f∖i=∅
172 171 a1i ⊢k∈𝒫g∩f∖i×b∖j∧k:f∖i⟶1-1V→i∩f∖i=∅
173 incom ⊢j∩ran⁡k=ran⁡k∩j
174 159 117 sstrdi ⊢k∈𝒫g∩f∖i×b∖j→k⊆f∖i×b∖j
175 rnss ⊢k⊆f∖i×b∖j→ran⁡k⊆ran⁡f∖i×b∖j
176 rnxpss ⊢ran⁡f∖i×b∖j⊆b∖j
177 175 176 sstrdi ⊢k⊆f∖i×b∖j→ran⁡k⊆b∖j
178 174 177 syl ⊢k∈𝒫g∩f∖i×b∖j→ran⁡k⊆b∖j
179 disjdifr ⊢b∖j∩j=∅
180 ssdisj ⊢ran⁡k⊆b∖j∧b∖j∩j=∅→ran⁡k∩j=∅
181 178 179 180 sylancl ⊢k∈𝒫g∩f∖i×b∖j→ran⁡k∩j=∅
182 173 181 eqtrid ⊢k∈𝒫g∩f∖i×b∖j→j∩ran⁡k=∅
183 182 adantr ⊢k∈𝒫g∩f∖i×b∖j∧k:f∖i⟶1-1V→j∩ran⁡k=∅
184 f1oun ⊢ij:i⟶1-1 ontoj∧k:f∖i⟶1-1 ontoran⁡k∧i∩f∖i=∅∧j∩ran⁡k=∅→ij∪k:i∪f∖i⟶1-1 ontoj∪ran⁡k
185 168 170 172 183 184 syl22anc ⊢k∈𝒫g∩f∖i×b∖j∧k:f∖i⟶1-1V→ij∪k:i∪f∖i⟶1-1 ontoj∪ran⁡k
186 185 adantl ⊢g∈𝒫f×b∧i∈f∧j∈gi∧k∈𝒫g∩f∖i×b∖j∧k:f∖i⟶1-1V→ij∪k:i∪f∖i⟶1-1 ontoj∪ran⁡k
187 snssi ⊢i∈f→i⊆f
188 187 ad2antrl ⊢g∈𝒫f×b∧i∈f∧j∈gi→i⊆f
189 undif ⊢i⊆f↔i∪f∖i=f
190 188 189 sylib ⊢g∈𝒫f×b∧i∈f∧j∈gi→i∪f∖i=f
191 190 f1oeq2d ⊢g∈𝒫f×b∧i∈f∧j∈gi→ij∪k:i∪f∖i⟶1-1 ontoj∪ran⁡k↔ij∪k:f⟶1-1 ontoj∪ran⁡k
192 191 adantr ⊢g∈𝒫f×b∧i∈f∧j∈gi∧k∈𝒫g∩f∖i×b∖j∧k:f∖i⟶1-1V→ij∪k:i∪f∖i⟶1-1 ontoj∪ran⁡k↔ij∪k:f⟶1-1 ontoj∪ran⁡k
193 186 192 mpbid ⊢g∈𝒫f×b∧i∈f∧j∈gi∧k∈𝒫g∩f∖i×b∖j∧k:f∖i⟶1-1V→ij∪k:f⟶1-1 ontoj∪ran⁡k
194 f1of1 ⊢ij∪k:f⟶1-1 ontoj∪ran⁡k→ij∪k:f⟶1-1j∪ran⁡k
195 ssv ⊢j∪ran⁡k⊆V
196 f1ss ⊢ij∪k:f⟶1-1j∪ran⁡k∧j∪ran⁡k⊆V→ij∪k:f⟶1-1V
197 194 195 196 sylancl ⊢ij∪k:f⟶1-1 ontoj∪ran⁡k→ij∪k:f⟶1-1V
198 193 197 syl ⊢g∈𝒫f×b∧i∈f∧j∈gi∧k∈𝒫g∩f∖i×b∖j∧k:f∖i⟶1-1V→ij∪k:f⟶1-1V
199 f1eq1 ⊢e=ij∪k→e:f⟶1-1V↔ij∪k:f⟶1-1V
200 199 rspcev ⊢ij∪k∈𝒫g∧ij∪k:f⟶1-1V→∃e∈𝒫ge:f⟶1-1V
201 166 198 200 syl2anc ⊢g∈𝒫f×b∧i∈f∧j∈gi∧k∈𝒫g∩f∖i×b∖j∧k:f∖i⟶1-1V→∃e∈𝒫ge:f⟶1-1V
202 201 rexlimdvaa ⊢g∈𝒫f×b∧i∈f∧j∈gi→∃k∈𝒫g∩f∖i×b∖jk:f∖i⟶1-1V→∃e∈𝒫ge:f⟶1-1V
203 202 ex ⊢g∈𝒫f×b→i∈f∧j∈gi→∃k∈𝒫g∩f∖i×b∖jk:f∖i⟶1-1V→∃e∈𝒫ge:f⟶1-1V
204 203 adantr ⊢g∈𝒫f×b∧∀d∈𝒫fd≼gd→i∈f∧j∈gi→∃k∈𝒫g∩f∖i×b∖jk:f∖i⟶1-1V→∃e∈𝒫ge:f⟶1-1V
205 204 ad2antlr ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh→i∈f∧j∈gi→∃k∈𝒫g∩f∖i×b∖jk:f∖i⟶1-1V→∃e∈𝒫ge:f⟶1-1V
206 205 impr ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi→∃k∈𝒫g∩f∖i×b∖jk:f∖i⟶1-1V→∃e∈𝒫ge:f⟶1-1V
207 206 adantllr ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi→∃k∈𝒫g∩f∖i×b∖jk:f∖i⟶1-1V→∃e∈𝒫ge:f⟶1-1V
208 153 207 mpd ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f∧j∈gi→∃e∈𝒫ge:f⟶1-1V
209 208 expr ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh→i∈f∧j∈gi→∃e∈𝒫ge:f⟶1-1V
210 209 expd ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh→i∈f→j∈gi→∃e∈𝒫ge:f⟶1-1V
211 210 impr ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f→j∈gi→∃e∈𝒫ge:f⟶1-1V
212 211 exlimdv ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f→∃jj∈gi→∃e∈𝒫ge:f⟶1-1V
213 56 212 mpd ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh∧i∈f→∃e∈𝒫ge:f⟶1-1V
214 213 expr ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh→i∈f→∃e∈𝒫ge:f⟶1-1V
215 214 exlimdv ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh→∃ii∈f→∃e∈𝒫ge:f⟶1-1V
216 32 215 biimtrid ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh→f≠∅→∃e∈𝒫ge:f⟶1-1V
217 31 216 pm2.61dne ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∀hh⊂f∧h≠∅→h≺gh→∃e∈𝒫ge:f⟶1-1V
218 exanali ⊢∃hh⊂f∧h≠∅∧¬h≺gh↔¬∀hh⊂f∧h≠∅→h≺gh
219 simprll ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→h⊂f
220 pssss ⊢h⊂f→h⊆f
221 219 220 syl ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→h⊆f
222 221 sspwd ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→𝒫h⊆𝒫f
223 simplrr ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∀d∈𝒫fd≼gd
224 ssralv ⊢𝒫h⊆𝒫f→∀d∈𝒫fd≼gd→∀d∈𝒫hd≼gd
225 222 223 224 sylc ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∀d∈𝒫hd≼gd
226 elpwi ⊢d∈𝒫h→d⊆h
227 resima2 ⊢d⊆h→g↾hd=gd
228 226 227 syl ⊢d∈𝒫h→g↾hd=gd
229 228 eqcomd ⊢d∈𝒫h→gd=g↾hd
230 229 breq2d ⊢d∈𝒫h→d≼gd↔d≼g↾hd
231 230 ralbiia ⊢∀d∈𝒫hd≼gd↔∀d∈𝒫hd≼g↾hd
232 225 231 sylib ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∀d∈𝒫hd≼g↾hd
233 imaeq1 ⊢c=g↾h→cd=g↾hd
234 233 breq2d ⊢c=g↾h→d≼cd↔d≼g↾hd
235 234 ralbidv ⊢c=g↾h→∀d∈𝒫hd≼cd↔∀d∈𝒫hd≼g↾hd
236 pweq ⊢c=g↾h→𝒫c=𝒫g↾h
237 236 rexeqdv ⊢c=g↾h→∃e∈𝒫ce:h⟶1-1V↔∃e∈𝒫g↾he:h⟶1-1V
238 235 237 imbi12d ⊢c=g↾h→∀d∈𝒫hd≼cd→∃e∈𝒫ce:h⟶1-1V↔∀d∈𝒫hd≼g↾hd→∃e∈𝒫g↾he:h⟶1-1V
239 simpllr ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V
240 psseq1 ⊢a=h→a⊂f↔h⊂f
241 xpeq1 ⊢a=h→a×b=h×b
242 241 pweqd ⊢a=h→𝒫a×b=𝒫h×b
243 pweq ⊢a=h→𝒫a=𝒫h
244 243 raleqdv ⊢a=h→∀d∈𝒫ad≼cd↔∀d∈𝒫hd≼cd
245 f1eq2 ⊢a=h→e:a⟶1-1V↔e:h⟶1-1V
246 245 rexbidv ⊢a=h→∃e∈𝒫ce:a⟶1-1V↔∃e∈𝒫ce:h⟶1-1V
247 244 246 imbi12d ⊢a=h→∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔∀d∈𝒫hd≼cd→∃e∈𝒫ce:h⟶1-1V
248 242 247 raleqbidv ⊢a=h→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔∀c∈𝒫h×b∀d∈𝒫hd≼cd→∃e∈𝒫ce:h⟶1-1V
249 240 248 imbi12d ⊢a=h→a⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔h⊂f→∀c∈𝒫h×b∀d∈𝒫hd≼cd→∃e∈𝒫ce:h⟶1-1V
250 249 spvv ⊢∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V→h⊂f→∀c∈𝒫h×b∀d∈𝒫hd≼cd→∃e∈𝒫ce:h⟶1-1V
251 239 219 250 sylc ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∀c∈𝒫h×b∀d∈𝒫hd≼cd→∃e∈𝒫ce:h⟶1-1V
252 simplrl ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→g∈𝒫f×b
253 ssres ⊢g⊆f×b→g↾h⊆f×b↾h
254 df-res ⊢f×b↾h=f×b∩h×V
255 inxp ⊢f×b∩h×V=f∩h×b∩V
256 inss2 ⊢f∩h⊆h
257 inss1 ⊢b∩V⊆b
258 xpss12 ⊢f∩h⊆h∧b∩V⊆b→f∩h×b∩V⊆h×b
259 256 257 258 mp2an ⊢f∩h×b∩V⊆h×b
260 255 259 eqsstri ⊢f×b∩h×V⊆h×b
261 254 260 eqsstri ⊢f×b↾h⊆h×b
262 253 261 sstrdi ⊢g⊆f×b→g↾h⊆h×b
263 94 262 syl ⊢g∈𝒫f×b→g↾h⊆h×b
264 45 resex ⊢g↾h∈V
265 264 elpw ⊢g↾h∈𝒫h×b↔g↾h⊆h×b
266 263 265 sylibr ⊢g∈𝒫f×b→g↾h∈𝒫h×b
267 252 266 syl ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→g↾h∈𝒫h×b
268 238 251 267 rspcdva ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∀d∈𝒫hd≼g↾hd→∃e∈𝒫g↾he:h⟶1-1V
269 232 268 mpd ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∃e∈𝒫g↾he:h⟶1-1V
270 f1eq1 ⊢e=i→e:h⟶1-1V↔i:h⟶1-1V
271 270 cbvrexvw ⊢∃e∈𝒫g↾he:h⟶1-1V↔∃i∈𝒫g↾hi:h⟶1-1V
272 269 271 sylib ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∃i∈𝒫g↾hi:h⟶1-1V
273 id ⊢d=h∪c→d=h∪c
274 imaeq2 ⊢d=h∪c→gd=gh∪c
275 273 274 breq12d ⊢d=h∪c→d≼gd↔h∪c≼gh∪c
276 simprr ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd→∀d∈𝒫fd≼gd
277 276 ad2antrr ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→∀d∈𝒫fd≼gd
278 220 ad2antrr ⊢h⊂f∧h≠∅∧¬h≺gh→h⊆f
279 278 ad2antlr ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→h⊆f
280 elpwi ⊢c∈𝒫f∖h→c⊆f∖h
281 difss ⊢f∖h⊆f
282 280 281 sstrdi ⊢c∈𝒫f∖h→c⊆f
283 282 adantl ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→c⊆f
284 279 283 unssd ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→h∪c⊆f
285 128 elpw2 ⊢h∪c∈𝒫f↔h∪c⊆f
286 284 285 sylibr ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→h∪c∈𝒫f
287 275 277 286 rspcdva ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→h∪c≼gh∪c
288 imaundi ⊢gh∪c=gh∪gc
289 undif2 ⊢gh∪gc∖gh=gh∪gc
290 288 289 eqtr4i ⊢gh∪c=gh∪gc∖gh
291 287 290 breqtrdi ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→h∪c≼gh∪gc∖gh
292 simp-4l ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→f∈Fin
293 292 279 ssfid ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→h∈Fin
294 id ⊢d=h→d=h
295 imaeq2 ⊢d=h→gd=gh
296 294 295 breq12d ⊢d=h→d≼gd↔h≼gh
297 vex ⊢h∈V
298 297 elpw ⊢h∈𝒫f↔h⊆f
299 279 298 sylibr ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→h∈𝒫f
300 296 277 299 rspcdva ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→h≼gh
301 simplrr ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→¬h≺gh
302 bren2 ⊢h≈gh↔h≼gh∧¬h≺gh
303 300 301 302 sylanbrc ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→h≈gh
304 303 ensymd ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→gh≈h
305 incom ⊢h∩c=c∩h
306 ssdifin0 ⊢c⊆f∖h→c∩h=∅
307 305 306 eqtrid ⊢c⊆f∖h→h∩c=∅
308 280 307 syl ⊢c∈𝒫f∖h→h∩c=∅
309 308 adantl ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→h∩c=∅
310 disjdif ⊢gh∩gc∖gh=∅
311 310 a1i ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→gh∩gc∖gh=∅
312 domunfican ⊢h∈Fin∧gh≈h∧h∩c=∅∧gh∩gc∖gh=∅→h∪c≼gh∪gc∖gh↔c≼gc∖gh
313 293 304 309 311 312 syl22anc ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→h∪c≼gh∪gc∖gh↔c≼gc∖gh
314 291 313 mpbid ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→c≼gc∖gh
315 101 difeq1d ⊢g∈𝒫f×b→gc∩b∖gh=gc∖gh
316 315 ad2antrl ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd→gc∩b∖gh=gc∖gh
317 316 ad2antrr ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→gc∩b∖gh=gc∖gh
318 314 317 breqtrrd ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→c≼gc∩b∖gh
319 df-ss ⊢c⊆f∖h↔c∩f∖h=c
320 280 319 sylib ⊢c∈𝒫f∖h→c∩f∖h=c
321 320 imaeq2d ⊢c∈𝒫f∖h→gc∩f∖h=gc
322 321 ineq1d ⊢c∈𝒫f∖h→gc∩f∖h∩b∖gh=gc∩b∖gh
323 indif2 ⊢gc∩b∖gh=gc∩b∖gh
324 322 323 eqtrdi ⊢c∈𝒫f∖h→gc∩f∖h∩b∖gh=gc∩b∖gh
325 324 adantl ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→gc∩f∖h∩b∖gh=gc∩b∖gh
326 318 325 breqtrrd ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh∧c∈𝒫f∖h→c≼gc∩f∖h∩b∖gh
327 326 ralrimiva ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∀c∈𝒫f∖hc≼gc∩f∖h∩b∖gh
328 imainrect ⊢g∩f∖h×b∖ghc=gc∩f∖h∩b∖gh
329 imaeq2 ⊢c=d→g∩f∖h×b∖ghc=g∩f∖h×b∖ghd
330 328 329 eqtr3id ⊢c=d→gc∩f∖h∩b∖gh=g∩f∖h×b∖ghd
331 109 330 breq12d ⊢c=d→c≼gc∩f∖h∩b∖gh↔d≼g∩f∖h×b∖ghd
332 331 cbvralvw ⊢∀c∈𝒫f∖hc≼gc∩f∖h∩b∖gh↔∀d∈𝒫f∖hd≼g∩f∖h×b∖ghd
333 327 332 sylib ⊢f∈Fin∧b∈Fin∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∀d∈𝒫f∖hd≼g∩f∖h×b∖ghd
334 333 adantllr ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∀d∈𝒫f∖hd≼g∩f∖h×b∖ghd
335 inss2 ⊢g∩f∖h×b∖gh⊆f∖h×b∖gh
336 difss ⊢b∖gh⊆b
337 xpss2 ⊢b∖gh⊆b→f∖h×b∖gh⊆f∖h×b
338 336 337 ax-mp ⊢f∖h×b∖gh⊆f∖h×b
339 335 338 sstri ⊢g∩f∖h×b∖gh⊆f∖h×b
340 45 inex1 ⊢g∩f∖h×b∖gh∈V
341 340 elpw ⊢g∩f∖h×b∖gh∈𝒫f∖h×b↔g∩f∖h×b∖gh⊆f∖h×b
342 339 341 mpbir ⊢g∩f∖h×b∖gh∈𝒫f∖h×b
343 incom ⊢f∩h=h∩f
344 df-ss ⊢h⊆f↔h∩f=h
345 220 344 sylib ⊢h⊂f→h∩f=h
346 343 345 eqtrid ⊢h⊂f→f∩h=h
347 346 neeq1d ⊢h⊂f→f∩h≠∅↔h≠∅
348 347 biimpar ⊢h⊂f∧h≠∅→f∩h≠∅
349 disj4 ⊢f∩h=∅↔¬f∖h⊂f
350 349 bicomi ⊢¬f∖h⊂f↔f∩h=∅
351 350 necon1abii ⊢f∩h≠∅↔f∖h⊂f
352 348 351 sylib ⊢h⊂f∧h≠∅→f∖h⊂f
353 352 ad2antrl ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→f∖h⊂f
354 128 difexi ⊢f∖h∈V
355 psseq1 ⊢a=f∖h→a⊂f↔f∖h⊂f
356 xpeq1 ⊢a=f∖h→a×b=f∖h×b
357 356 pweqd ⊢a=f∖h→𝒫a×b=𝒫f∖h×b
358 pweq ⊢a=f∖h→𝒫a=𝒫f∖h
359 358 raleqdv ⊢a=f∖h→∀d∈𝒫ad≼cd↔∀d∈𝒫f∖hd≼cd
360 f1eq2 ⊢a=f∖h→e:a⟶1-1V↔e:f∖h⟶1-1V
361 360 rexbidv ⊢a=f∖h→∃e∈𝒫ce:a⟶1-1V↔∃e∈𝒫ce:f∖h⟶1-1V
362 359 361 imbi12d ⊢a=f∖h→∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔∀d∈𝒫f∖hd≼cd→∃e∈𝒫ce:f∖h⟶1-1V
363 357 362 raleqbidv ⊢a=f∖h→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔∀c∈𝒫f∖h×b∀d∈𝒫f∖hd≼cd→∃e∈𝒫ce:f∖h⟶1-1V
364 355 363 imbi12d ⊢a=f∖h→a⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V↔f∖h⊂f→∀c∈𝒫f∖h×b∀d∈𝒫f∖hd≼cd→∃e∈𝒫ce:f∖h⟶1-1V
365 354 364 spcv ⊢∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V→f∖h⊂f→∀c∈𝒫f∖h×b∀d∈𝒫f∖hd≼cd→∃e∈𝒫ce:f∖h⟶1-1V
366 239 353 365 sylc ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∀c∈𝒫f∖h×b∀d∈𝒫f∖hd≼cd→∃e∈𝒫ce:f∖h⟶1-1V
367 imaeq1 ⊢c=g∩f∖h×b∖gh→cd=g∩f∖h×b∖ghd
368 367 breq2d ⊢c=g∩f∖h×b∖gh→d≼cd↔d≼g∩f∖h×b∖ghd
369 368 ralbidv ⊢c=g∩f∖h×b∖gh→∀d∈𝒫f∖hd≼cd↔∀d∈𝒫f∖hd≼g∩f∖h×b∖ghd
370 pweq ⊢c=g∩f∖h×b∖gh→𝒫c=𝒫g∩f∖h×b∖gh
371 370 rexeqdv ⊢c=g∩f∖h×b∖gh→∃e∈𝒫ce:f∖h⟶1-1V↔∃e∈𝒫g∩f∖h×b∖ghe:f∖h⟶1-1V
372 369 371 imbi12d ⊢c=g∩f∖h×b∖gh→∀d∈𝒫f∖hd≼cd→∃e∈𝒫ce:f∖h⟶1-1V↔∀d∈𝒫f∖hd≼g∩f∖h×b∖ghd→∃e∈𝒫g∩f∖h×b∖ghe:f∖h⟶1-1V
373 372 rspcva ⊢g∩f∖h×b∖gh∈𝒫f∖h×b∧∀c∈𝒫f∖h×b∀d∈𝒫f∖hd≼cd→∃e∈𝒫ce:f∖h⟶1-1V→∀d∈𝒫f∖hd≼g∩f∖h×b∖ghd→∃e∈𝒫g∩f∖h×b∖ghe:f∖h⟶1-1V
374 342 366 373 sylancr ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∀d∈𝒫f∖hd≼g∩f∖h×b∖ghd→∃e∈𝒫g∩f∖h×b∖ghe:f∖h⟶1-1V
375 334 374 mpd ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∃e∈𝒫g∩f∖h×b∖ghe:f∖h⟶1-1V
376 f1eq1 ⊢e=j→e:f∖h⟶1-1V↔j:f∖h⟶1-1V
377 376 cbvrexvw ⊢∃e∈𝒫g∩f∖h×b∖ghe:f∖h⟶1-1V↔∃j∈𝒫g∩f∖h×b∖ghj:f∖h⟶1-1V
378 375 377 sylib ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∃j∈𝒫g∩f∖h×b∖ghj:f∖h⟶1-1V
379 elpwi ⊢i∈𝒫g↾h→i⊆g↾h
380 resss ⊢g↾h⊆g
381 379 380 sstrdi ⊢i∈𝒫g↾h→i⊆g
382 381 adantr ⊢i∈𝒫g↾h∧i:h⟶1-1V→i⊆g
383 382 ad2antlr ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→i⊆g
384 elpwi ⊢j∈𝒫g∩f∖h×b∖gh→j⊆g∩f∖h×b∖gh
385 inss1 ⊢g∩f∖h×b∖gh⊆g
386 384 385 sstrdi ⊢j∈𝒫g∩f∖h×b∖gh→j⊆g
387 386 ad2antrl ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→j⊆g
388 383 387 unssd ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→i∪j⊆g
389 45 elpw2 ⊢i∪j∈𝒫g↔i∪j⊆g
390 388 389 sylibr ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→i∪j∈𝒫g
391 f1f1orn ⊢i:h⟶1-1V→i:h⟶1-1 ontoran⁡i
392 391 adantl ⊢i∈𝒫g↾h∧i:h⟶1-1V→i:h⟶1-1 ontoran⁡i
393 392 ad2antlr ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→i:h⟶1-1 ontoran⁡i
394 f1f1orn ⊢j:f∖h⟶1-1V→j:f∖h⟶1-1 ontoran⁡j
395 394 ad2antll ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→j:f∖h⟶1-1 ontoran⁡j
396 disjdif ⊢h∩f∖h=∅
397 396 a1i ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→h∩f∖h=∅
398 rnss ⊢i⊆g↾h→ran⁡i⊆ran⁡g↾h
399 379 398 syl ⊢i∈𝒫g↾h→ran⁡i⊆ran⁡g↾h
400 df-ima ⊢gh=ran⁡g↾h
401 399 400 sseqtrrdi ⊢i∈𝒫g↾h→ran⁡i⊆gh
402 401 adantr ⊢i∈𝒫g↾h∧i:h⟶1-1V→ran⁡i⊆gh
403 402 ad2antlr ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→ran⁡i⊆gh
404 incom ⊢gh∩ran⁡j=ran⁡j∩gh
405 384 335 sstrdi ⊢j∈𝒫g∩f∖h×b∖gh→j⊆f∖h×b∖gh
406 rnss ⊢j⊆f∖h×b∖gh→ran⁡j⊆ran⁡f∖h×b∖gh
407 405 406 syl ⊢j∈𝒫g∩f∖h×b∖gh→ran⁡j⊆ran⁡f∖h×b∖gh
408 rnxpss ⊢ran⁡f∖h×b∖gh⊆b∖gh
409 407 408 sstrdi ⊢j∈𝒫g∩f∖h×b∖gh→ran⁡j⊆b∖gh
410 409 ad2antrl ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→ran⁡j⊆b∖gh
411 disjdifr ⊢b∖gh∩gh=∅
412 ssdisj ⊢ran⁡j⊆b∖gh∧b∖gh∩gh=∅→ran⁡j∩gh=∅
413 410 411 412 sylancl ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→ran⁡j∩gh=∅
414 404 413 eqtrid ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→gh∩ran⁡j=∅
415 ssdisj ⊢ran⁡i⊆gh∧gh∩ran⁡j=∅→ran⁡i∩ran⁡j=∅
416 403 414 415 syl2anc ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→ran⁡i∩ran⁡j=∅
417 f1oun ⊢i:h⟶1-1 ontoran⁡i∧j:f∖h⟶1-1 ontoran⁡j∧h∩f∖h=∅∧ran⁡i∩ran⁡j=∅→i∪j:h∪f∖h⟶1-1 ontoran⁡i∪ran⁡j
418 393 395 397 416 417 syl22anc ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→i∪j:h∪f∖h⟶1-1 ontoran⁡i∪ran⁡j
419 undif ⊢h⊆f↔h∪f∖h=f
420 419 biimpi ⊢h⊆f→h∪f∖h=f
421 420 adantl ⊢g∈𝒫f×b∧h⊆f→h∪f∖h=f
422 421 ad2antrr ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→h∪f∖h=f
423 422 f1oeq2d ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→i∪j:h∪f∖h⟶1-1 ontoran⁡i∪ran⁡j↔i∪j:f⟶1-1 ontoran⁡i∪ran⁡j
424 418 423 mpbid ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→i∪j:f⟶1-1 ontoran⁡i∪ran⁡j
425 f1of1 ⊢i∪j:f⟶1-1 ontoran⁡i∪ran⁡j→i∪j:f⟶1-1ran⁡i∪ran⁡j
426 424 425 syl ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→i∪j:f⟶1-1ran⁡i∪ran⁡j
427 ssv ⊢ran⁡i∪ran⁡j⊆V
428 f1ss ⊢i∪j:f⟶1-1ran⁡i∪ran⁡j∧ran⁡i∪ran⁡j⊆V→i∪j:f⟶1-1V
429 426 427 428 sylancl ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→i∪j:f⟶1-1V
430 f1eq1 ⊢e=i∪j→e:f⟶1-1V↔i∪j:f⟶1-1V
431 430 rspcev ⊢i∪j∈𝒫g∧i∪j:f⟶1-1V→∃e∈𝒫ge:f⟶1-1V
432 390 429 431 syl2anc ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V∧j∈𝒫g∩f∖h×b∖gh∧j:f∖h⟶1-1V→∃e∈𝒫ge:f⟶1-1V
433 432 rexlimdvaa ⊢g∈𝒫f×b∧h⊆f∧i∈𝒫g↾h∧i:h⟶1-1V→∃j∈𝒫g∩f∖h×b∖ghj:f∖h⟶1-1V→∃e∈𝒫ge:f⟶1-1V
434 433 rexlimdvaa ⊢g∈𝒫f×b∧h⊆f→∃i∈𝒫g↾hi:h⟶1-1V→∃j∈𝒫g∩f∖h×b∖ghj:f∖h⟶1-1V→∃e∈𝒫ge:f⟶1-1V
435 252 221 434 syl2anc ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∃i∈𝒫g↾hi:h⟶1-1V→∃j∈𝒫g∩f∖h×b∖ghj:f∖h⟶1-1V→∃e∈𝒫ge:f⟶1-1V
436 272 378 435 mp2d ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧h⊂f∧h≠∅∧¬h≺gh→∃e∈𝒫ge:f⟶1-1V
437 436 ex ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd→h⊂f∧h≠∅∧¬h≺gh→∃e∈𝒫ge:f⟶1-1V
438 437 exlimdv ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd→∃hh⊂f∧h≠∅∧¬h≺gh→∃e∈𝒫ge:f⟶1-1V
439 438 imp ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧∃hh⊂f∧h≠∅∧¬h≺gh→∃e∈𝒫ge:f⟶1-1V
440 218 439 sylan2br ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd∧¬∀hh⊂f∧h≠∅→h≺gh→∃e∈𝒫ge:f⟶1-1V
441 217 440 pm2.61dan ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V∧g∈𝒫f×b∧∀d∈𝒫fd≼gd→∃e∈𝒫ge:f⟶1-1V
442 441 exp32 ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V→g∈𝒫f×b→∀d∈𝒫fd≼gd→∃e∈𝒫ge:f⟶1-1V
443 442 ralrimiv ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V→∀g∈𝒫f×b∀d∈𝒫fd≼gd→∃e∈𝒫ge:f⟶1-1V
444 imaeq1 ⊢g=c→gd=cd
445 444 breq2d ⊢g=c→d≼gd↔d≼cd
446 445 ralbidv ⊢g=c→∀d∈𝒫fd≼gd↔∀d∈𝒫fd≼cd
447 pweq ⊢g=c→𝒫g=𝒫c
448 447 rexeqdv ⊢g=c→∃e∈𝒫ge:f⟶1-1V↔∃e∈𝒫ce:f⟶1-1V
449 446 448 imbi12d ⊢g=c→∀d∈𝒫fd≼gd→∃e∈𝒫ge:f⟶1-1V↔∀d∈𝒫fd≼cd→∃e∈𝒫ce:f⟶1-1V
450 449 cbvralvw ⊢∀g∈𝒫f×b∀d∈𝒫fd≼gd→∃e∈𝒫ge:f⟶1-1V↔∀c∈𝒫f×b∀d∈𝒫fd≼cd→∃e∈𝒫ce:f⟶1-1V
451 443 450 sylib ⊢f∈Fin∧b∈Fin∧∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V→∀c∈𝒫f×b∀d∈𝒫fd≼cd→∃e∈𝒫ce:f⟶1-1V
452 451 exp31 ⊢f∈Fin→b∈Fin→∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V→∀c∈𝒫f×b∀d∈𝒫fd≼cd→∃e∈𝒫ce:f⟶1-1V
453 452 a2d ⊢f∈Fin→b∈Fin→∀aa⊂f→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V→b∈Fin→∀c∈𝒫f×b∀d∈𝒫fd≼cd→∃e∈𝒫ce:f⟶1-1V
454 22 453 biimtrid ⊢f∈Fin→∀aa⊂f→b∈Fin→∀c∈𝒫a×b∀d∈𝒫ad≼cd→∃e∈𝒫ce:a⟶1-1V→b∈Fin→∀c∈𝒫f×b∀d∈𝒫fd≼cd→∃e∈𝒫ce:f⟶1-1V
455 9 18 454 findcard3 ⊢A∈Fin→b∈Fin→∀c∈𝒫A×b∀d∈𝒫Ad≼cd→∃e∈𝒫ce:A⟶1-1V