MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  marypha1lem Structured version   Visualization version   GIF version

Theorem marypha1lem 8380
Description: Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015.)
Assertion
Ref Expression
marypha1lem (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V)))
Distinct variable group:   𝐴,𝑏,𝑐,𝑑,𝑒

Proof of Theorem marypha1lem
Dummy variables 𝑎 𝑓 𝑔 𝑖 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xpeq1 5157 . . . . 5 (𝑎 = 𝑓 → (𝑎 × 𝑏) = (𝑓 × 𝑏))
21pweqd 4196 . . . 4 (𝑎 = 𝑓 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝑓 × 𝑏))
3 pweq 4194 . . . . . 6 (𝑎 = 𝑓 → 𝒫 𝑎 = 𝒫 𝑓)
43raleqdv 3174 . . . . 5 (𝑎 = 𝑓 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑)))
5 f1eq2 6135 . . . . . 6 (𝑎 = 𝑓 → (𝑒:𝑎1-1→V ↔ 𝑒:𝑓1-1→V))
65rexbidv 3081 . . . . 5 (𝑎 = 𝑓 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))
74, 6imbi12d 333 . . . 4 (𝑎 = 𝑓 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V)))
82, 7raleqbidv 3182 . . 3 (𝑎 = 𝑓 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V)))
98imbi2d 329 . 2 (𝑎 = 𝑓 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))))
10 xpeq1 5157 . . . . 5 (𝑎 = 𝐴 → (𝑎 × 𝑏) = (𝐴 × 𝑏))
1110pweqd 4196 . . . 4 (𝑎 = 𝐴 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝐴 × 𝑏))
12 pweq 4194 . . . . . 6 (𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴)
1312raleqdv 3174 . . . . 5 (𝑎 = 𝐴 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑)))
14 f1eq2 6135 . . . . . 6 (𝑎 = 𝐴 → (𝑒:𝑎1-1→V ↔ 𝑒:𝐴1-1→V))
1514rexbidv 3081 . . . . 5 (𝑎 = 𝐴 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V))
1613, 15imbi12d 333 . . . 4 (𝑎 = 𝐴 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V)))
1711, 16raleqbidv 3182 . . 3 (𝑎 = 𝐴 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V)))
1817imbi2d 329 . 2 (𝑎 = 𝐴 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V))))
19 bi2.04 375 . . . . 5 ((𝑎𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ↔ (𝑏 ∈ Fin → (𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))))
2019albii 1787 . . . 4 (∀𝑎(𝑎𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ↔ ∀𝑎(𝑏 ∈ Fin → (𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))))
21 19.21v 1908 . . . 4 (∀𝑎(𝑏 ∈ Fin → (𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))))
2220, 21bitri 264 . . 3 (∀𝑎(𝑎𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))))
23 0elpw 4864 . . . . . . . . . . . . 13 ∅ ∈ 𝒫 𝑔
24 f10 6207 . . . . . . . . . . . . 13 ∅:∅–1-1→V
25 f1eq1 6134 . . . . . . . . . . . . . 14 (𝑒 = ∅ → (𝑒:∅–1-1→V ↔ ∅:∅–1-1→V))
2625rspcev 3340 . . . . . . . . . . . . 13 ((∅ ∈ 𝒫 𝑔 ∧ ∅:∅–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V)
2723, 24, 26mp2an 708 . . . . . . . . . . . 12 𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V
28 f1eq2 6135 . . . . . . . . . . . . 13 (𝑓 = ∅ → (𝑒:𝑓1-1→V ↔ 𝑒:∅–1-1→V))
2928rexbidv 3081 . . . . . . . . . . . 12 (𝑓 = ∅ → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V))
3027, 29mpbiri 248 . . . . . . . . . . 11 (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
3130a1i 11 . . . . . . . . . 10 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
32 n0 3964 . . . . . . . . . . 11 (𝑓 ≠ ∅ ↔ ∃𝑖 𝑖𝑓)
33 snelpwi 4942 . . . . . . . . . . . . . . . . . . 19 (𝑖𝑓 → {𝑖} ∈ 𝒫 𝑓)
34 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = {𝑖} → 𝑑 = {𝑖})
35 imaeq2 5497 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = {𝑖} → (𝑔𝑑) = (𝑔 “ {𝑖}))
3634, 35breq12d 4698 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 = {𝑖} → (𝑑 ≼ (𝑔𝑑) ↔ {𝑖} ≼ (𝑔 “ {𝑖})))
3736rspcva 3338 . . . . . . . . . . . . . . . . . . . . 21 (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → {𝑖} ≼ (𝑔 “ {𝑖}))
38 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑖 ∈ V
3938snnz 4340 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑖} ≠ ∅
40 snex 4938 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑖} ∈ V
41400sdom 8132 . . . . . . . . . . . . . . . . . . . . . . . 24 (∅ ≺ {𝑖} ↔ {𝑖} ≠ ∅)
4239, 41mpbir 221 . . . . . . . . . . . . . . . . . . . . . . 23 ∅ ≺ {𝑖}
43 sdomdomtr 8134 . . . . . . . . . . . . . . . . . . . . . . 23 ((∅ ≺ {𝑖} ∧ {𝑖} ≼ (𝑔 “ {𝑖})) → ∅ ≺ (𝑔 “ {𝑖}))
4442, 43mpan 706 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑖} ≼ (𝑔 “ {𝑖}) → ∅ ≺ (𝑔 “ {𝑖}))
45 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑔 ∈ V
4645imaex 7146 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 “ {𝑖}) ∈ V
47460sdom 8132 . . . . . . . . . . . . . . . . . . . . . 22 (∅ ≺ (𝑔 “ {𝑖}) ↔ (𝑔 “ {𝑖}) ≠ ∅)
4844, 47sylib 208 . . . . . . . . . . . . . . . . . . . . 21 ({𝑖} ≼ (𝑔 “ {𝑖}) → (𝑔 “ {𝑖}) ≠ ∅)
4937, 48syl 17 . . . . . . . . . . . . . . . . . . . 20 (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → (𝑔 “ {𝑖}) ≠ ∅)
5049expcom 450 . . . . . . . . . . . . . . . . . . 19 (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ({𝑖} ∈ 𝒫 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
5133, 50syl5 34 . . . . . . . . . . . . . . . . . 18 (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → (𝑖𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
5251adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → (𝑖𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
5352ad2antlr 763 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑖𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
5453impr 648 . . . . . . . . . . . . . . 15 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → (𝑔 “ {𝑖}) ≠ ∅)
55 n0 3964 . . . . . . . . . . . . . . 15 ((𝑔 “ {𝑖}) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
5654, 55sylib 208 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
5745imaex 7146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔𝑐) ∈ V
5857difexi 4842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔𝑐) ∖ {𝑗}) ∈ V
59580dom 8131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ ≼ ((𝑔𝑐) ∖ {𝑗})
60 breq1 4688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = ∅ → (𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}) ↔ ∅ ≼ ((𝑔𝑐) ∖ {𝑗})))
6159, 60mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = ∅ → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
6261a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 = ∅ → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗})))
63 simpll 805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → ∀((𝑓 ≠ ∅) → ≺ (𝑔)))
64 elpwi 4201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
6564ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
66 difsnpss 4370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓)
6766biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖𝑓 → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
6867ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
6965, 68sspsstrd 3748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐𝑓)
70 simprr 811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≠ ∅)
7169, 70jca 553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑐𝑓𝑐 ≠ ∅))
72 psseq1 3727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑐 → (𝑓𝑐𝑓))
73 neeq1 2885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑐 → ( ≠ ∅ ↔ 𝑐 ≠ ∅))
7472, 73anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( = 𝑐 → ((𝑓 ≠ ∅) ↔ (𝑐𝑓𝑐 ≠ ∅)))
75 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑐 = 𝑐)
76 imaeq2 5497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑐 → (𝑔) = (𝑔𝑐))
7775, 76breq12d 4698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( = 𝑐 → ( ≺ (𝑔) ↔ 𝑐 ≺ (𝑔𝑐)))
7874, 77imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ( = 𝑐 → (((𝑓 ≠ ∅) → ≺ (𝑔)) ↔ ((𝑐𝑓𝑐 ≠ ∅) → 𝑐 ≺ (𝑔𝑐))))
7978spv 2296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀((𝑓 ≠ ∅) → ≺ (𝑔)) → ((𝑐𝑓𝑐 ≠ ∅) → 𝑐 ≺ (𝑔𝑐)))
8063, 71, 79sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≺ (𝑔𝑐))
81 domdifsn 8084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ≺ (𝑔𝑐) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
8280, 81syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
8382expr 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 ≠ ∅ → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗})))
8462, 83pm2.61dne 2909 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
8584adantlrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
8685adantll 750 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
87 df-ss 3621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ⊆ (𝑓 ∖ {𝑖}) ↔ (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
8864, 87sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
8988imaeq2d 5501 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) = (𝑔𝑐))
9089ineq1d 3846 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})))
9190adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})))
92 indif2 3903 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})) = (((𝑔𝑐) ∩ 𝑏) ∖ {𝑗})
93 imassrn 5512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔𝑐) ⊆ ran 𝑔
94 elpwi 4201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → 𝑔 ⊆ (𝑓 × 𝑏))
95 rnss 5386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔 ⊆ ran (𝑓 × 𝑏))
96 rnxpss 5601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ran (𝑓 × 𝑏) ⊆ 𝑏
9795, 96syl6ss 3648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔𝑏)
9894, 97syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ran 𝑔𝑏)
9993, 98syl5ss 3647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔𝑐) ⊆ 𝑏)
100 df-ss 3621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔𝑐) ⊆ 𝑏 ↔ ((𝑔𝑐) ∩ 𝑏) = (𝑔𝑐))
10199, 100sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑔𝑐) ∩ 𝑏) = (𝑔𝑐))
102101difeq1d 3760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔𝑐) ∖ {𝑗}))
103102ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → (((𝑔𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔𝑐) ∖ {𝑗}))
10492, 103syl5eq 2697 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∖ {𝑗}))
105104ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∖ {𝑗}))
10691, 105eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∖ {𝑗}))
10786, 106breqtrrd 4713 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
108107ralrimiva 2995 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
109 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑑𝑐 = 𝑑)
110 imainrect 5610 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗}))
111 imaeq2 5497 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
112110, 111syl5eqr 2699 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
113109, 112breq12d 4698 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
114113cbvralv 3201 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
115108, 114sylib 208 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
116115adantllr 755 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
117 inss2 3867 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))
118 difss 3770 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 ∖ {𝑗}) ⊆ 𝑏
119 xpss2 5162 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 ∖ {𝑗}) ⊆ 𝑏 → ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
120118, 119ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
121117, 120sstri 3645 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
12245inex1 4832 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ V
123122elpw 4197 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ↔ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
124121, 123mpbir 221 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)
125 simpllr 815 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)))
12667adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
127126ad2antll 765 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
128 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑓 ∈ V
129128difexi 4842 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 ∖ {𝑖}) ∈ V
130 psseq1 3727 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓))
131 xpeq1 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎 × 𝑏) = ((𝑓 ∖ {𝑖}) × 𝑏))
132131pweqd 4196 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏))
133 pweq 4194 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 𝑎 = 𝒫 (𝑓 ∖ {𝑖}))
134133raleqdv 3174 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑)))
135 f1eq2 6135 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = (𝑓 ∖ {𝑖}) → (𝑒:𝑎1-1→V ↔ 𝑒:(𝑓 ∖ {𝑖})–1-1→V))
136135rexbidv 3081 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝑓 ∖ {𝑖}) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
137134, 136imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (𝑓 ∖ {𝑖}) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
138132, 137raleqbidv 3182 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
139130, 138imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑓 ∖ {𝑖}) → ((𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))))
140129, 139spcv 3330 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) → ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
141125, 127, 140sylc 65 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
142 imaeq1 5496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑐𝑑) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
143142breq2d 4697 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑑 ≼ (𝑐𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
144143ralbidv 3015 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
145 pweq 4194 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
146145rexeqdv 3175 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
147144, 146imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ((∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
148147rspcva 3338 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
149124, 141, 148sylancr 696 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
150116, 149mpd 15 . . . . . . . . . . . . . . . . . . . 20 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)
151 f1eq1 6134 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = 𝑘 → (𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ 𝑘:(𝑓 ∖ {𝑖})–1-1→V))
152151cbvrexv 3202 . . . . . . . . . . . . . . . . . . . 20 (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
153150, 152sylib 208 . . . . . . . . . . . . . . . . . . 19 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
154 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑗 ∈ V
15538, 154elimasn 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (𝑔 “ {𝑖}) ↔ ⟨𝑖, 𝑗⟩ ∈ 𝑔)
156155biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (𝑔 “ {𝑖}) → ⟨𝑖, 𝑗⟩ ∈ 𝑔)
157156snssd 4372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (𝑔 “ {𝑖}) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
158157ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
159 elpwi 4201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
160 inss1 3866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ 𝑔
161159, 160syl6ss 3648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘𝑔)
162161adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → 𝑘𝑔)
163158, 162unssd 3822 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
16445elpw2 4858 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
165163, 164sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
166165ad2ant2lr 799 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
16738, 154f1osn 6214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗}
168167a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗})
169 f1f1orn 6186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘:(𝑓 ∖ {𝑖})–1-1→V → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
170169adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
171 disjdif 4073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅
172171a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅)
173 incom 3838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ({𝑗} ∩ ran 𝑘) = (ran 𝑘 ∩ {𝑗})
174159, 117syl6ss 3648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
175 rnss 5386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
176 rnxpss 5601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ (𝑏 ∖ {𝑗})
177175, 176syl6ss 3648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
178174, 177syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
179 incom 3838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ({𝑗} ∩ (𝑏 ∖ {𝑗}))
180 disjdif 4073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ({𝑗} ∩ (𝑏 ∖ {𝑗})) = ∅
181179, 180eqtri 2673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅
182 ssdisj 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((ran 𝑘 ⊆ (𝑏 ∖ {𝑗}) ∧ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅) → (ran 𝑘 ∩ {𝑗}) = ∅)
183178, 181, 182sylancl 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (ran 𝑘 ∩ {𝑗}) = ∅)
184173, 183syl5eq 2697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ({𝑗} ∩ ran 𝑘) = ∅)
185184adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑗} ∩ ran 𝑘) = ∅)
186 f1oun 6194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((({⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗} ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘) ∧ (({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅ ∧ ({𝑗} ∩ ran 𝑘) = ∅)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
187168, 170, 172, 185, 186syl22anc 1367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
188187adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
189 snssi 4371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖𝑓 → {𝑖} ⊆ 𝑓)
190189ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) → {𝑖} ⊆ 𝑓)
191 undif 4082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ({𝑖} ⊆ 𝑓 ↔ ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
192190, 191sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) → ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
193 f1oeq2 6166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓 → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘)))
194192, 193syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘)))
195194adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘)))
196188, 195mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘))
197 f1of1 6174 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→({𝑗} ∪ ran 𝑘))
198 ssv 3658 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({𝑗} ∪ ran 𝑘) ⊆ V
199 f1ss 6144 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→({𝑗} ∪ ran 𝑘) ∧ ({𝑗} ∪ ran 𝑘) ⊆ V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V)
200197, 198, 199sylancl 695 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V)
201196, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V)
202 f1eq1 6134 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑒 = ({⟨𝑖, 𝑗⟩} ∪ 𝑘) → (𝑒:𝑓1-1→V ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V))
203202rspcev 3340 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ∧ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
204166, 201, 203syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
205204rexlimdvaa 3061 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
206205ex 449 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
207206adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
208207ad2antlr 763 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
209208impr 648 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
210209adantllr 755 . . . . . . . . . . . . . . . . . . 19 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
211153, 210mpd 15 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
212211expr 642 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
213212expd 451 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑖𝑓 → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
214213impr 648 . . . . . . . . . . . . . . 15 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
215214exlimdv 1901 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → (∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
21656, 215mpd 15 . . . . . . . . . . . . 13 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
217216expr 642 . . . . . . . . . . . 12 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑖𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
218217exlimdv 1901 . . . . . . . . . . 11 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (∃𝑖 𝑖𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
21932, 218syl5bi 232 . . . . . . . . . 10 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑓 ≠ ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
22031, 219pm2.61dne 2909 . . . . . . . . 9 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
221 exanali 1826 . . . . . . . . . 10 (∃((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔)) ↔ ¬ ∀((𝑓 ≠ ∅) → ≺ (𝑔)))
222 simprll 819 . . . . . . . . . . . . . . . . . . . 20 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → 𝑓)
223 pssss 3735 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑓)
224222, 223syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → 𝑓)
225 sspwb 4947 . . . . . . . . . . . . . . . . . . 19 (𝑓 ↔ 𝒫 ⊆ 𝒫 𝑓)
226224, 225sylib 208 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → 𝒫 ⊆ 𝒫 𝑓)
227 simplrr 818 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))
228 ssralv 3699 . . . . . . . . . . . . . . . . . 18 (𝒫 ⊆ 𝒫 𝑓 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑔𝑑)))
229226, 227, 228sylc 65 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑔𝑑))
230 elpwi 4201 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ 𝒫 𝑑)
231 resima2 5467 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 → ((𝑔) “ 𝑑) = (𝑔𝑑))
232230, 231syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑑 ∈ 𝒫 → ((𝑔) “ 𝑑) = (𝑔𝑑))
233232eqcomd 2657 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ 𝒫 → (𝑔𝑑) = ((𝑔) “ 𝑑))
234233breq2d 4697 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ 𝒫 → (𝑑 ≼ (𝑔𝑑) ↔ 𝑑 ≼ ((𝑔) “ 𝑑)))
235234ralbiia 3008 . . . . . . . . . . . . . . . . 17 (∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑔𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑))
236229, 235sylib 208 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑))
237 simplrl 817 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → 𝑔 ∈ 𝒫 (𝑓 × 𝑏))
238 ssres 5459 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔) ⊆ ((𝑓 × 𝑏) ↾ ))
239 df-res 5155 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 × 𝑏) ↾ ) = ((𝑓 × 𝑏) ∩ ( × V))
240 inxp 5287 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 × 𝑏) ∩ ( × V)) = ((𝑓) × (𝑏 ∩ V))
241 inss2 3867 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓) ⊆
242 inss1 3866 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 ∩ V) ⊆ 𝑏
243 xpss12 5158 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓) ⊆ ∧ (𝑏 ∩ V) ⊆ 𝑏) → ((𝑓) × (𝑏 ∩ V)) ⊆ ( × 𝑏))
244241, 242, 243mp2an 708 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓) × (𝑏 ∩ V)) ⊆ ( × 𝑏)
245240, 244eqsstri 3668 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 × 𝑏) ∩ ( × V)) ⊆ ( × 𝑏)
246239, 245eqsstri 3668 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 × 𝑏) ↾ ) ⊆ ( × 𝑏)
247238, 246syl6ss 3648 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔) ⊆ ( × 𝑏))
24894, 247syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔) ⊆ ( × 𝑏))
24945resex 5478 . . . . . . . . . . . . . . . . . . . 20 (𝑔) ∈ V
250249elpw 4197 . . . . . . . . . . . . . . . . . . 19 ((𝑔) ∈ 𝒫 ( × 𝑏) ↔ (𝑔) ⊆ ( × 𝑏))
251248, 250sylibr 224 . . . . . . . . . . . . . . . . . 18 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔) ∈ 𝒫 ( × 𝑏))
252237, 251syl 17 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (𝑔) ∈ 𝒫 ( × 𝑏))
253 simpllr 815 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)))
254 psseq1 3727 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = → (𝑎𝑓𝑓))
255 xpeq1 5157 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = → (𝑎 × 𝑏) = ( × 𝑏))
256255pweqd 4196 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = → 𝒫 (𝑎 × 𝑏) = 𝒫 ( × 𝑏))
257 pweq 4194 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = → 𝒫 𝑎 = 𝒫 )
258257raleqdv 3174 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑)))
259 f1eq2 6135 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = → (𝑒:𝑎1-1→V ↔ 𝑒:1-1→V))
260259rexbidv 3081 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V))
261258, 260imbi12d 333 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V)))
262256, 261raleqbidv 3182 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 ( × 𝑏)(∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V)))
263254, 262imbi12d 333 . . . . . . . . . . . . . . . . . . 19 (𝑎 = → ((𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ (𝑓 → ∀𝑐 ∈ 𝒫 ( × 𝑏)(∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V))))
264263spv 2296 . . . . . . . . . . . . . . . . . 18 (∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) → (𝑓 → ∀𝑐 ∈ 𝒫 ( × 𝑏)(∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V)))
265253, 222, 264sylc 65 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑐 ∈ 𝒫 ( × 𝑏)(∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V))
266 imaeq1 5496 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = (𝑔) → (𝑐𝑑) = ((𝑔) “ 𝑑))
267266breq2d 4697 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑔) → (𝑑 ≼ (𝑐𝑑) ↔ 𝑑 ≼ ((𝑔) “ 𝑑)))
268267ralbidv 3015 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑔) → (∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑)))
269 pweq 4194 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑔) → 𝒫 𝑐 = 𝒫 (𝑔))
270269rexeqdv 3175 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑔) → (∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V))
271268, 270imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝑔) → ((∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V)))
272271rspcva 3338 . . . . . . . . . . . . . . . . 17 (((𝑔) ∈ 𝒫 ( × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ( × 𝑏)(∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V)) → (∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V))
273252, 265, 272syl2anc 694 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V))
274236, 273mpd 15 . . . . . . . . . . . . . . 15 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V)
275 f1eq1 6134 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑖 → (𝑒:1-1→V ↔ 𝑖:1-1→V))
276275cbvrexv 3202 . . . . . . . . . . . . . . 15 (∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V ↔ ∃𝑖 ∈ 𝒫 (𝑔)𝑖:1-1→V)
277274, 276sylib 208 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑖 ∈ 𝒫 (𝑔)𝑖:1-1→V)
278223ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔)) → 𝑓)
279278ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑓)
280 elpwi 4201 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ 𝒫 (𝑓) → 𝑐 ⊆ (𝑓))
281 difss 3770 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓) ⊆ 𝑓
282280, 281syl6ss 3648 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ 𝒫 (𝑓) → 𝑐𝑓)
283282adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑐𝑓)
284279, 283unssd 3822 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) ⊆ 𝑓)
285128elpw2 4858 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐) ∈ 𝒫 𝑓 ↔ (𝑐) ⊆ 𝑓)
286284, 285sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) ∈ 𝒫 𝑓)
287 simprr 811 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))
288287ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))
289 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = (𝑐) → 𝑑 = (𝑐))
290 imaeq2 5497 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = (𝑐) → (𝑔𝑑) = (𝑔 “ (𝑐)))
291289, 290breq12d 4698 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑐) → (𝑑 ≼ (𝑔𝑑) ↔ (𝑐) ≼ (𝑔 “ (𝑐))))
292291rspcva 3338 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑐) ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → (𝑐) ≼ (𝑔 “ (𝑐)))
293286, 288, 292syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) ≼ (𝑔 “ (𝑐)))
294 imaundi 5580 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 “ (𝑐)) = ((𝑔) ∪ (𝑔𝑐))
295 undif2 4077 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔))) = ((𝑔) ∪ (𝑔𝑐))
296294, 295eqtr4i 2676 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 “ (𝑐)) = ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔)))
297293, 296syl6breq 4726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) ≼ ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔))))
298 simp-4l 823 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑓 ∈ Fin)
299298, 279ssfid 8224 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ∈ Fin)
300 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ∈ V
301300elpw 4197 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ 𝒫 𝑓𝑓)
302279, 301sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ∈ 𝒫 𝑓)
303 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = 𝑑 = )
304 imaeq2 5497 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = → (𝑔𝑑) = (𝑔))
305303, 304breq12d 4698 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = → (𝑑 ≼ (𝑔𝑑) ↔ ≼ (𝑔)))
306305rspcva 3338 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → ≼ (𝑔))
307302, 288, 306syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ≼ (𝑔))
308 simplrr 818 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ¬ ≺ (𝑔))
309 bren2 8028 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( ≈ (𝑔) ↔ ( ≼ (𝑔) ∧ ¬ ≺ (𝑔)))
310307, 308, 309sylanbrc 699 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ≈ (𝑔))
311310ensymd 8048 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑔) ≈ )
312 incom 3838 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐) = (𝑐)
313 ssdifin0 4083 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 ⊆ (𝑓) → (𝑐) = ∅)
314312, 313syl5eq 2697 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 ⊆ (𝑓) → (𝑐) = ∅)
315280, 314syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 ∈ 𝒫 (𝑓) → (𝑐) = ∅)
316315adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) = ∅)
317 disjdif 4073 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔) ∩ ((𝑔𝑐) ∖ (𝑔))) = ∅
318317a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ((𝑔) ∩ ((𝑔𝑐) ∖ (𝑔))) = ∅)
319 domunfican 8274 . . . . . . . . . . . . . . . . . . . . . . 23 ((( ∈ Fin ∧ (𝑔) ≈ ) ∧ ((𝑐) = ∅ ∧ ((𝑔) ∩ ((𝑔𝑐) ∖ (𝑔))) = ∅)) → ((𝑐) ≼ ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔))) ↔ 𝑐 ≼ ((𝑔𝑐) ∖ (𝑔))))
320299, 311, 316, 318, 319syl22anc 1367 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ((𝑐) ≼ ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔))) ↔ 𝑐 ≼ ((𝑔𝑐) ∖ (𝑔))))
321297, 320mpbid 222 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑐 ≼ ((𝑔𝑐) ∖ (𝑔)))
322101difeq1d 3760 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)) = ((𝑔𝑐) ∖ (𝑔)))
323322ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)) = ((𝑔𝑐) ∖ (𝑔)))
324323ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)) = ((𝑔𝑐) ∖ (𝑔)))
325321, 324breqtrrd 4713 . . . . . . . . . . . . . . . . . . . 20 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑐 ≼ (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)))
326 df-ss 3621 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 ⊆ (𝑓) ↔ (𝑐 ∩ (𝑓)) = 𝑐)
327280, 326sylib 208 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 ∈ 𝒫 (𝑓) → (𝑐 ∩ (𝑓)) = 𝑐)
328327imaeq2d 5501 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 ∈ 𝒫 (𝑓) → (𝑔 “ (𝑐 ∩ (𝑓))) = (𝑔𝑐))
329328ineq1d 3846 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ 𝒫 (𝑓) → ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) = ((𝑔𝑐) ∩ (𝑏 ∖ (𝑔))))
330 indif2 3903 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔𝑐) ∩ (𝑏 ∖ (𝑔))) = (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔))
331329, 330syl6eq 2701 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 ∈ 𝒫 (𝑓) → ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) = (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)))
332331adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) = (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)))
333325, 332breqtrrd 4713 . . . . . . . . . . . . . . . . . . 19 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))))
334333ralrimiva 2995 . . . . . . . . . . . . . . . . . 18 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑐 ∈ 𝒫 (𝑓)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))))
335 imainrect 5610 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔)))
336 imaeq2 5497 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑐) = ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
337335, 336syl5eqr 2699 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) = ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
338109, 337breq12d 4698 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑)))
339338cbvralv 3201 . . . . . . . . . . . . . . . . . 18 (∀𝑐 ∈ 𝒫 (𝑓)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) ↔ ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
340334, 339sylib 208 . . . . . . . . . . . . . . . . 17 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
341340adantllr 755 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
342 inss2 3867 . . . . . . . . . . . . . . . . . . 19 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ⊆ ((𝑓) × (𝑏 ∖ (𝑔)))
343 difss 3770 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∖ (𝑔)) ⊆ 𝑏
344 xpss2 5162 . . . . . . . . . . . . . . . . . . . 20 ((𝑏 ∖ (𝑔)) ⊆ 𝑏 → ((𝑓) × (𝑏 ∖ (𝑔))) ⊆ ((𝑓) × 𝑏))
345343, 344ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑓) × (𝑏 ∖ (𝑔))) ⊆ ((𝑓) × 𝑏)
346342, 345sstri 3645 . . . . . . . . . . . . . . . . . 18 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ⊆ ((𝑓) × 𝑏)
34745inex1 4832 . . . . . . . . . . . . . . . . . . 19 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∈ V
348347elpw 4197 . . . . . . . . . . . . . . . . . 18 ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∈ 𝒫 ((𝑓) × 𝑏) ↔ (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ⊆ ((𝑓) × 𝑏))
349346, 348mpbir 221 . . . . . . . . . . . . . . . . 17 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∈ 𝒫 ((𝑓) × 𝑏)
350 incom 3838 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓) = (𝑓)
351 df-ss 3621 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 ↔ (𝑓) = )
352223, 351sylib 208 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 → (𝑓) = )
353350, 352syl5eq 2697 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 → (𝑓) = )
354353neeq1d 2882 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 → ((𝑓) ≠ ∅ ↔ ≠ ∅))
355354biimpar 501 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ≠ ∅) → (𝑓) ≠ ∅)
356 disj4 4058 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓) = ∅ ↔ ¬ (𝑓) ⊊ 𝑓)
357356bicomi 214 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑓) ⊊ 𝑓 ↔ (𝑓) = ∅)
358357necon1abii 2871 . . . . . . . . . . . . . . . . . . . 20 ((𝑓) ≠ ∅ ↔ (𝑓) ⊊ 𝑓)
359355, 358sylib 208 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ≠ ∅) → (𝑓) ⊊ 𝑓)
360359ad2antrl 764 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (𝑓) ⊊ 𝑓)
361128difexi 4842 . . . . . . . . . . . . . . . . . . 19 (𝑓) ∈ V
362 psseq1 3727 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑓) → (𝑎𝑓 ↔ (𝑓) ⊊ 𝑓))
363 xpeq1 5157 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑓) → (𝑎 × 𝑏) = ((𝑓) × 𝑏))
364363pweqd 4196 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑓) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓) × 𝑏))
365 pweq 4194 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑓) → 𝒫 𝑎 = 𝒫 (𝑓))
366365raleqdv 3174 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑓) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑)))
367 f1eq2 6135 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑓) → (𝑒:𝑎1-1→V ↔ 𝑒:(𝑓)–1-1→V))
368367rexbidv 3081 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑓) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V))
369366, 368imbi12d 333 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑓) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V)))
370364, 369raleqbidv 3182 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑓) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V)))
371362, 370imbi12d 333 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑓) → ((𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ ((𝑓) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V))))
372361, 371spcv 3330 . . . . . . . . . . . . . . . . . 18 (∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) → ((𝑓) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V)))
373253, 360, 372sylc 65 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V))
374 imaeq1 5496 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → (𝑐𝑑) = ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
375374breq2d 4697 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → (𝑑 ≼ (𝑐𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑)))
376375ralbidv 3015 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑)))
377 pweq 4194 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))))
378377rexeqdv 3175 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V))
379376, 378imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → ((∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V)))
380379rspcva 3338 . . . . . . . . . . . . . . . . 17 (((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∈ 𝒫 ((𝑓) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V))
381349, 373, 380sylancr 696 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V))
382341, 381mpd 15 . . . . . . . . . . . . . . 15 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V)
383 f1eq1 6134 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑗 → (𝑒:(𝑓)–1-1→V ↔ 𝑗:(𝑓)–1-1→V))
384383cbvrexv 3202 . . . . . . . . . . . . . . 15 (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V ↔ ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V)
385382, 384sylib 208 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V)
386 elpwi 4201 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ 𝒫 (𝑔) → 𝑖 ⊆ (𝑔))
387 resss 5457 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔) ⊆ 𝑔
388386, 387syl6ss 3648 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ 𝒫 (𝑔) → 𝑖𝑔)
389388adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V) → 𝑖𝑔)
390389ad2antlr 763 . . . . . . . . . . . . . . . . . . . 20 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → 𝑖𝑔)
391 elpwi 4201 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → 𝑗 ⊆ (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))))
392 inss1 3866 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ⊆ 𝑔
393391, 392syl6ss 3648 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → 𝑗𝑔)
394393ad2antrl 764 . . . . . . . . . . . . . . . . . . . 20 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → 𝑗𝑔)
395390, 394unssd 3822 . . . . . . . . . . . . . . . . . . 19 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗) ⊆ 𝑔)
39645elpw2 4858 . . . . . . . . . . . . . . . . . . 19 ((𝑖𝑗) ∈ 𝒫 𝑔 ↔ (𝑖𝑗) ⊆ 𝑔)
397395, 396sylibr 224 . . . . . . . . . . . . . . . . . 18 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗) ∈ 𝒫 𝑔)
398 f1f1orn 6186 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖:1-1→V → 𝑖:1-1-onto→ran 𝑖)
399398adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V) → 𝑖:1-1-onto→ran 𝑖)
400399ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → 𝑖:1-1-onto→ran 𝑖)
401 f1f1orn 6186 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗:(𝑓)–1-1→V → 𝑗:(𝑓)–1-1-onto→ran 𝑗)
402401ad2antll 765 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → 𝑗:(𝑓)–1-1-onto→ran 𝑗)
403 disjdif 4073 . . . . . . . . . . . . . . . . . . . . . . 23 ( ∩ (𝑓)) = ∅
404403a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ( ∩ (𝑓)) = ∅)
405 rnss 5386 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ⊆ (𝑔) → ran 𝑖 ⊆ ran (𝑔))
406386, 405syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ 𝒫 (𝑔) → ran 𝑖 ⊆ ran (𝑔))
407 df-ima 5156 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔) = ran (𝑔)
408406, 407syl6sseqr 3685 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ 𝒫 (𝑔) → ran 𝑖 ⊆ (𝑔))
409408adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V) → ran 𝑖 ⊆ (𝑔))
410409ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ran 𝑖 ⊆ (𝑔))
411 incom 3838 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔) ∩ ran 𝑗) = (ran 𝑗 ∩ (𝑔))
412391, 342syl6ss 3648 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → 𝑗 ⊆ ((𝑓) × (𝑏 ∖ (𝑔))))
413 rnss 5386 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ⊆ ((𝑓) × (𝑏 ∖ (𝑔))) → ran 𝑗 ⊆ ran ((𝑓) × (𝑏 ∖ (𝑔))))
414412, 413syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → ran 𝑗 ⊆ ran ((𝑓) × (𝑏 ∖ (𝑔))))
415 rnxpss 5601 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ran ((𝑓) × (𝑏 ∖ (𝑔))) ⊆ (𝑏 ∖ (𝑔))
416414, 415syl6ss 3648 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔)))
417416ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔)))
418 incom 3838 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏 ∖ (𝑔)) ∩ (𝑔)) = ((𝑔) ∩ (𝑏 ∖ (𝑔)))
419 disjdif 4073 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔) ∩ (𝑏 ∖ (𝑔))) = ∅
420418, 419eqtri 2673 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 ∖ (𝑔)) ∩ (𝑔)) = ∅
421 ssdisj 4059 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ran 𝑗 ⊆ (𝑏 ∖ (𝑔)) ∧ ((𝑏 ∖ (𝑔)) ∩ (𝑔)) = ∅) → (ran 𝑗 ∩ (𝑔)) = ∅)
422417, 420, 421sylancl 695 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (ran 𝑗 ∩ (𝑔)) = ∅)
423411, 422syl5eq 2697 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ((𝑔) ∩ ran 𝑗) = ∅)
424 ssdisj 4059 . . . . . . . . . . . . . . . . . . . . . . 23 ((ran 𝑖 ⊆ (𝑔) ∧ ((𝑔) ∩ ran 𝑗) = ∅) → (ran 𝑖 ∩ ran 𝑗) = ∅)
425410, 423, 424syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (ran 𝑖 ∩ ran 𝑗) = ∅)
426 f1oun 6194 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑖:1-1-onto→ran 𝑖𝑗:(𝑓)–1-1-onto→ran 𝑗) ∧ (( ∩ (𝑓)) = ∅ ∧ (ran 𝑖 ∩ ran 𝑗) = ∅)) → (𝑖𝑗):( ∪ (𝑓))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
427400, 402, 404, 425, 426syl22anc 1367 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗):( ∪ (𝑓))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
428 undif 4082 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 ↔ ( ∪ (𝑓)) = 𝑓)
429428biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 → ( ∪ (𝑓)) = 𝑓)
430429adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) → ( ∪ (𝑓)) = 𝑓)
431430ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ( ∪ (𝑓)) = 𝑓)
432 f1oeq2 6166 . . . . . . . . . . . . . . . . . . . . . 22 (( ∪ (𝑓)) = 𝑓 → ((𝑖𝑗):( ∪ (𝑓))–1-1-onto→(ran 𝑖 ∪ ran 𝑗) ↔ (𝑖𝑗):𝑓1-1-onto→(ran 𝑖 ∪ ran 𝑗)))
433431, 432syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ((𝑖𝑗):( ∪ (𝑓))–1-1-onto→(ran 𝑖 ∪ ran 𝑗) ↔ (𝑖𝑗):𝑓1-1-onto→(ran 𝑖 ∪ ran 𝑗)))
434427, 433mpbid 222 . . . . . . . . . . . . . . . . . . . 20 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗):𝑓1-1-onto→(ran 𝑖 ∪ ran 𝑗))
435 f1of1 6174 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑗):𝑓1-1-onto→(ran 𝑖 ∪ ran 𝑗) → (𝑖𝑗):𝑓1-1→(ran 𝑖 ∪ ran 𝑗))
436434, 435syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗):𝑓1-1→(ran 𝑖 ∪ ran 𝑗))
437 ssv 3658 . . . . . . . . . . . . . . . . . . 19 (ran 𝑖 ∪ ran 𝑗) ⊆ V
438 f1ss 6144 . . . . . . . . . . . . . . . . . . 19 (((𝑖𝑗):𝑓1-1→(ran 𝑖 ∪ ran 𝑗) ∧ (ran 𝑖 ∪ ran 𝑗) ⊆ V) → (𝑖𝑗):𝑓1-1→V)
439436, 437, 438sylancl 695 . . . . . . . . . . . . . . . . . 18 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗):𝑓1-1→V)
440 f1eq1 6134 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑖𝑗) → (𝑒:𝑓1-1→V ↔ (𝑖𝑗):𝑓1-1→V))
441440rspcev 3340 . . . . . . . . . . . . . . . . . 18 (((𝑖𝑗) ∈ 𝒫 𝑔 ∧ (𝑖𝑗):𝑓1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
442397, 439, 441syl2anc 694 . . . . . . . . . . . . . . . . 17 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
443442rexlimdvaa 3061 . . . . . . . . . . . . . . . 16 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
444443rexlimdvaa 3061 . . . . . . . . . . . . . . 15 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) → (∃𝑖 ∈ 𝒫 (𝑔)𝑖:1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
445237, 224, 444syl2anc 694 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (∃𝑖 ∈ 𝒫 (𝑔)𝑖:1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
446277, 385, 445mp2d 49 . . . . . . . . . . . . 13 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
447446ex 449 . . . . . . . . . . . 12 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → (((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
448447exlimdv 1901 . . . . . . . . . . 11 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → (∃((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
449448imp 444 . . . . . . . . . 10 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∃((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
450221, 449sylan2br 492 . . . . . . . . 9 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ¬ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
451220, 450pm2.61dan 849 . . . . . . . 8 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
452451exp32 630 . . . . . . 7 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
453452ralrimiv 2994 . . . . . 6 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → ∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
454 imaeq1 5496 . . . . . . . . . 10 (𝑔 = 𝑐 → (𝑔𝑑) = (𝑐𝑑))
455454breq2d 4697 . . . . . . . . 9 (𝑔 = 𝑐 → (𝑑 ≼ (𝑔𝑑) ↔ 𝑑 ≼ (𝑐𝑑)))
456455ralbidv 3015 . . . . . . . 8 (𝑔 = 𝑐 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑)))
457 pweq 4194 . . . . . . . . 9 (𝑔 = 𝑐 → 𝒫 𝑔 = 𝒫 𝑐)
458457rexeqdv 3175 . . . . . . . 8 (𝑔 = 𝑐 → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))
459456, 458imbi12d 333 . . . . . . 7 (𝑔 = 𝑐 → ((∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V)))
460459cbvralv 3201 . . . . . 6 (∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))
461453, 460sylib 208 . . . . 5 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))
462461exp31 629 . . . 4 (𝑓 ∈ Fin → (𝑏 ∈ Fin → (∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))))
463462a2d 29 . . 3 (𝑓 ∈ Fin → ((𝑏 ∈ Fin → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))))
46422, 463syl5bi 232 . 2 (𝑓 ∈ Fin → (∀𝑎(𝑎𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))))
4659, 18, 464findcard3 8244 1 (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  wal 1521   = wceq 1523  wex 1744  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  wpss 3608  c0 3948  𝒫 cpw 4191  {csn 4210  cop 4216   class class class wbr 4685   × cxp 5141  ran crn 5144  cres 5145  cima 5146  1-1wf1 5923  1-1-ontowf1o 5925  cen 7994  cdom 7995  csdm 7996  Fincfn 7997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-om 7108  df-1o 7605  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001
This theorem is referenced by:  marypha1  8381
  Copyright terms: Public domain W3C validator