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

Theorem marypha1lem 8881
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 5533 . . . . 5 (𝑎 = 𝑓 → (𝑎 × 𝑏) = (𝑓 × 𝑏))
21pweqd 4516 . . . 4 (𝑎 = 𝑓 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝑓 × 𝑏))
3 pweq 4513 . . . . . 6 (𝑎 = 𝑓 → 𝒫 𝑎 = 𝒫 𝑓)
43raleqdv 3364 . . . . 5 (𝑎 = 𝑓 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑)))
5 f1eq2 6545 . . . . . 6 (𝑎 = 𝑓 → (𝑒:𝑎1-1→V ↔ 𝑒:𝑓1-1→V))
65rexbidv 3256 . . . . 5 (𝑎 = 𝑓 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))
74, 6imbi12d 348 . . . 4 (𝑎 = 𝑓 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V)))
82, 7raleqbidv 3354 . . 3 (𝑎 = 𝑓 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V)))
98imbi2d 344 . 2 (𝑎 = 𝑓 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))))
10 xpeq1 5533 . . . . 5 (𝑎 = 𝐴 → (𝑎 × 𝑏) = (𝐴 × 𝑏))
1110pweqd 4516 . . . 4 (𝑎 = 𝐴 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝐴 × 𝑏))
12 pweq 4513 . . . . . 6 (𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴)
1312raleqdv 3364 . . . . 5 (𝑎 = 𝐴 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑)))
14 f1eq2 6545 . . . . . 6 (𝑎 = 𝐴 → (𝑒:𝑎1-1→V ↔ 𝑒:𝐴1-1→V))
1514rexbidv 3256 . . . . 5 (𝑎 = 𝐴 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V))
1613, 15imbi12d 348 . . . 4 (𝑎 = 𝐴 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V)))
1711, 16raleqbidv 3354 . . 3 (𝑎 = 𝐴 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V)))
1817imbi2d 344 . 2 (𝑎 = 𝐴 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V))))
19 bi2.04 392 . . . . 5 ((𝑎𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ↔ (𝑏 ∈ Fin → (𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))))
2019albii 1821 . . . 4 (∀𝑎(𝑎𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ↔ ∀𝑎(𝑏 ∈ Fin → (𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))))
21 19.21v 1940 . . . 4 (∀𝑎(𝑏 ∈ Fin → (𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))))
2220, 21bitri 278 . . 3 (∀𝑎(𝑎𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))))
23 0elpw 5221 . . . . . . . . . . . . 13 ∅ ∈ 𝒫 𝑔
24 f10 6622 . . . . . . . . . . . . 13 ∅:∅–1-1→V
25 f1eq1 6544 . . . . . . . . . . . . . 14 (𝑒 = ∅ → (𝑒:∅–1-1→V ↔ ∅:∅–1-1→V))
2625rspcev 3571 . . . . . . . . . . . . 13 ((∅ ∈ 𝒫 𝑔 ∧ ∅:∅–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V)
2723, 24, 26mp2an 691 . . . . . . . . . . . 12 𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V
28 f1eq2 6545 . . . . . . . . . . . . 13 (𝑓 = ∅ → (𝑒:𝑓1-1→V ↔ 𝑒:∅–1-1→V))
2928rexbidv 3256 . . . . . . . . . . . 12 (𝑓 = ∅ → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V))
3027, 29mpbiri 261 . . . . . . . . . . 11 (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
3130a1i 11 . . . . . . . . . 10 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
32 n0 4260 . . . . . . . . . . 11 (𝑓 ≠ ∅ ↔ ∃𝑖 𝑖𝑓)
33 snelpwi 5302 . . . . . . . . . . . . . . . . . . 19 (𝑖𝑓 → {𝑖} ∈ 𝒫 𝑓)
34 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = {𝑖} → 𝑑 = {𝑖})
35 imaeq2 5892 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = {𝑖} → (𝑔𝑑) = (𝑔 “ {𝑖}))
3634, 35breq12d 5043 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 = {𝑖} → (𝑑 ≼ (𝑔𝑑) ↔ {𝑖} ≼ (𝑔 “ {𝑖})))
3736rspcva 3569 . . . . . . . . . . . . . . . . . . . . 21 (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → {𝑖} ≼ (𝑔 “ {𝑖}))
38 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑖 ∈ V
3938snnz 4672 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑖} ≠ ∅
40 snex 5297 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑖} ∈ V
41400sdom 8632 . . . . . . . . . . . . . . . . . . . . . . . 24 (∅ ≺ {𝑖} ↔ {𝑖} ≠ ∅)
4239, 41mpbir 234 . . . . . . . . . . . . . . . . . . . . . . 23 ∅ ≺ {𝑖}
43 sdomdomtr 8634 . . . . . . . . . . . . . . . . . . . . . . 23 ((∅ ≺ {𝑖} ∧ {𝑖} ≼ (𝑔 “ {𝑖})) → ∅ ≺ (𝑔 “ {𝑖}))
4442, 43mpan 689 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑖} ≼ (𝑔 “ {𝑖}) → ∅ ≺ (𝑔 “ {𝑖}))
45 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑔 ∈ V
4645imaex 7603 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 “ {𝑖}) ∈ V
47460sdom 8632 . . . . . . . . . . . . . . . . . . . . . 22 (∅ ≺ (𝑔 “ {𝑖}) ↔ (𝑔 “ {𝑖}) ≠ ∅)
4844, 47sylib 221 . . . . . . . . . . . . . . . . . . . . 21 ({𝑖} ≼ (𝑔 “ {𝑖}) → (𝑔 “ {𝑖}) ≠ ∅)
4937, 48syl 17 . . . . . . . . . . . . . . . . . . . 20 (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → (𝑔 “ {𝑖}) ≠ ∅)
5049expcom 417 . . . . . . . . . . . . . . . . . . 19 (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ({𝑖} ∈ 𝒫 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
5133, 50syl5 34 . . . . . . . . . . . . . . . . . 18 (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → (𝑖𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
5251adantl 485 . . . . . . . . . . . . . . . . 17 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → (𝑖𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
5352ad2antlr 726 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑖𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
5453impr 458 . . . . . . . . . . . . . . 15 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → (𝑔 “ {𝑖}) ≠ ∅)
55 n0 4260 . . . . . . . . . . . . . . 15 ((𝑔 “ {𝑖}) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
5654, 55sylib 221 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
5745imaex 7603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔𝑐) ∈ V
5857difexi 5196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔𝑐) ∖ {𝑗}) ∈ V
59580dom 8631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ ≼ ((𝑔𝑐) ∖ {𝑗})
60 breq1 5033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = ∅ → (𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}) ↔ ∅ ≼ ((𝑔𝑐) ∖ {𝑗})))
6159, 60mpbiri 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = ∅ → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
6261a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 = ∅ → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗})))
63 simpll 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → ∀((𝑓 ≠ ∅) → ≺ (𝑔)))
64 elpwi 4506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
6564ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
66 difsnpss 4700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓)
6766biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖𝑓 → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
6867ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
6965, 68sspsstrd 4036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐𝑓)
70 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≠ ∅)
7169, 70jca 515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑐𝑓𝑐 ≠ ∅))
72 psseq1 4015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑐 → (𝑓𝑐𝑓))
73 neeq1 3049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑐 → ( ≠ ∅ ↔ 𝑐 ≠ ∅))
7472, 73anbi12d 633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( = 𝑐 → ((𝑓 ≠ ∅) ↔ (𝑐𝑓𝑐 ≠ ∅)))
75 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑐 = 𝑐)
76 imaeq2 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑐 → (𝑔) = (𝑔𝑐))
7775, 76breq12d 5043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( = 𝑐 → ( ≺ (𝑔) ↔ 𝑐 ≺ (𝑔𝑐)))
7874, 77imbi12d 348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ( = 𝑐 → (((𝑓 ≠ ∅) → ≺ (𝑔)) ↔ ((𝑐𝑓𝑐 ≠ ∅) → 𝑐 ≺ (𝑔𝑐))))
7978spvv 2003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀((𝑓 ≠ ∅) → ≺ (𝑔)) → ((𝑐𝑓𝑐 ≠ ∅) → 𝑐 ≺ (𝑔𝑐)))
8063, 71, 79sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≺ (𝑔𝑐))
81 domdifsn 8583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ≺ (𝑔𝑐) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
8280, 81syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
8382expr 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 ≠ ∅ → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗})))
8462, 83pm2.61dne 3073 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
8584adantlrr 720 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
8685adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
87 df-ss 3898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ⊆ (𝑓 ∖ {𝑖}) ↔ (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
8864, 87sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
8988imaeq2d 5896 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) = (𝑔𝑐))
9089ineq1d 4138 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})))
9190adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})))
92 indif2 4197 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})) = (((𝑔𝑐) ∩ 𝑏) ∖ {𝑗})
93 imassrn 5907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔𝑐) ⊆ ran 𝑔
94 elpwi 4506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → 𝑔 ⊆ (𝑓 × 𝑏))
95 rnss 5773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔 ⊆ ran (𝑓 × 𝑏))
96 rnxpss 5996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ran (𝑓 × 𝑏) ⊆ 𝑏
9795, 96sstrdi 3927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔𝑏)
9894, 97syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ran 𝑔𝑏)
9993, 98sstrid 3926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔𝑐) ⊆ 𝑏)
100 df-ss 3898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔𝑐) ⊆ 𝑏 ↔ ((𝑔𝑐) ∩ 𝑏) = (𝑔𝑐))
10199, 100sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑔𝑐) ∩ 𝑏) = (𝑔𝑐))
102101difeq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔𝑐) ∖ {𝑗}))
103102ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → (((𝑔𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔𝑐) ∖ {𝑗}))
10492, 103syl5eq 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∖ {𝑗}))
105104ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∖ {𝑗}))
10691, 105eqtrd 2833 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∖ {𝑗}))
10786, 106breqtrrd 5058 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
108107ralrimiva 3149 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
109 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑑𝑐 = 𝑑)
110 imainrect 6005 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗}))
111 imaeq2 5892 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
112110, 111syl5eqr 2847 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
113109, 112breq12d 5043 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
114113cbvralvw 3396 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
115108, 114sylib 221 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
116115adantllr 718 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
117 inss2 4156 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))
118 difss 4059 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 ∖ {𝑗}) ⊆ 𝑏
119 xpss2 5539 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 ∖ {𝑗}) ⊆ 𝑏 → ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
120118, 119ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
121117, 120sstri 3924 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
12245inex1 5185 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ V
123122elpw 4501 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ↔ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
124121, 123mpbir 234 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)
125 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)))
12667adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
127126ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
128 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑓 ∈ V
129128difexi 5196 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 ∖ {𝑖}) ∈ V
130 psseq1 4015 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓))
131 xpeq1 5533 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎 × 𝑏) = ((𝑓 ∖ {𝑖}) × 𝑏))
132131pweqd 4516 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏))
133 pweq 4513 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 𝑎 = 𝒫 (𝑓 ∖ {𝑖}))
134133raleqdv 3364 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑)))
135 f1eq2 6545 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = (𝑓 ∖ {𝑖}) → (𝑒:𝑎1-1→V ↔ 𝑒:(𝑓 ∖ {𝑖})–1-1→V))
136135rexbidv 3256 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝑓 ∖ {𝑖}) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
137134, 136imbi12d 348 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (𝑓 ∖ {𝑖}) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
138132, 137raleqbidv 3354 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
139130, 138imbi12d 348 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑓 ∖ {𝑖}) → ((𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))))
140129, 139spcv 3554 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) → ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
141125, 127, 140sylc 65 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
142 imaeq1 5891 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑐𝑑) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
143142breq2d 5042 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑑 ≼ (𝑐𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
144143ralbidv 3162 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
145 pweq 4513 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
146145rexeqdv 3365 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
147144, 146imbi12d 348 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ((∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
148147rspcva 3569 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
149124, 141, 148sylancr 590 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
150116, 149mpd 15 . . . . . . . . . . . . . . . . . . . 20 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)
151 f1eq1 6544 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = 𝑘 → (𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ 𝑘:(𝑓 ∖ {𝑖})–1-1→V))
152151cbvrexvw 3397 . . . . . . . . . . . . . . . . . . . 20 (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
153150, 152sylib 221 . . . . . . . . . . . . . . . . . . 19 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
154 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑗 ∈ V
15538, 154elimasn 5921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (𝑔 “ {𝑖}) ↔ ⟨𝑖, 𝑗⟩ ∈ 𝑔)
156155biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (𝑔 “ {𝑖}) → ⟨𝑖, 𝑗⟩ ∈ 𝑔)
157156snssd 4702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (𝑔 “ {𝑖}) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
158157ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
159 elpwi 4506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
160 inss1 4155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ 𝑔
161159, 160sstrdi 3927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘𝑔)
162161adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → 𝑘𝑔)
163158, 162unssd 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
16445elpw2 5212 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
165163, 164sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
166165ad2ant2lr 747 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
16738, 154f1osn 6629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗}
168167a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗})
169 f1f1orn 6601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘:(𝑓 ∖ {𝑖})–1-1→V → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
170169adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
171 disjdif 4379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅
172171a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅)
173 incom 4128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ({𝑗} ∩ ran 𝑘) = (ran 𝑘 ∩ {𝑗})
174159, 117sstrdi 3927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
175 rnss 5773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
176 rnxpss 5996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ (𝑏 ∖ {𝑗})
177175, 176sstrdi 3927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
178174, 177syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
179 incom 4128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ({𝑗} ∩ (𝑏 ∖ {𝑗}))
180 disjdif 4379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ({𝑗} ∩ (𝑏 ∖ {𝑗})) = ∅
181179, 180eqtri 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅
182 ssdisj 4367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((ran 𝑘 ⊆ (𝑏 ∖ {𝑗}) ∧ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅) → (ran 𝑘 ∩ {𝑗}) = ∅)
183178, 181, 182sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (ran 𝑘 ∩ {𝑗}) = ∅)
184173, 183syl5eq 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ({𝑗} ∩ ran 𝑘) = ∅)
185184adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑗} ∩ ran 𝑘) = ∅)
186 f1oun 6609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((({⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗} ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘) ∧ (({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅ ∧ ({𝑗} ∩ ran 𝑘) = ∅)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
187168, 170, 172, 185, 186syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
188187adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
189 snssi 4701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖𝑓 → {𝑖} ⊆ 𝑓)
190189ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) → {𝑖} ⊆ 𝑓)
191 undif 4388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ({𝑖} ⊆ 𝑓 ↔ ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
192190, 191sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) → ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
193192f1oeq2d 6586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘)))
194193adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘)))
195188, 194mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘))
196 f1of1 6589 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→({𝑗} ∪ ran 𝑘))
197 ssv 3939 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({𝑗} ∪ ran 𝑘) ⊆ V
198 f1ss 6555 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→({𝑗} ∪ ran 𝑘) ∧ ({𝑗} ∪ ran 𝑘) ⊆ V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V)
199196, 197, 198sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V)
200195, 199syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V)
201 f1eq1 6544 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑒 = ({⟨𝑖, 𝑗⟩} ∪ 𝑘) → (𝑒:𝑓1-1→V ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V))
202201rspcev 3571 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ∧ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
203166, 200, 202syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
204203rexlimdvaa 3244 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
205204ex 416 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
206205adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
207206ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
208207impr 458 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
209208adantllr 718 . . . . . . . . . . . . . . . . . . 19 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
210153, 209mpd 15 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
211210expr 460 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
212211expd 419 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑖𝑓 → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
213212impr 458 . . . . . . . . . . . . . . 15 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
214213exlimdv 1934 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → (∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
21556, 214mpd 15 . . . . . . . . . . . . 13 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
216215expr 460 . . . . . . . . . . . 12 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑖𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
217216exlimdv 1934 . . . . . . . . . . 11 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (∃𝑖 𝑖𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
21832, 217syl5bi 245 . . . . . . . . . 10 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑓 ≠ ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
21931, 218pm2.61dne 3073 . . . . . . . . 9 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
220 exanali 1860 . . . . . . . . . 10 (∃((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔)) ↔ ¬ ∀((𝑓 ≠ ∅) → ≺ (𝑔)))
221 simprll 778 . . . . . . . . . . . . . . . . . . . 20 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → 𝑓)
222 pssss 4023 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑓)
223221, 222syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → 𝑓)
224223sspwd 4512 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → 𝒫 ⊆ 𝒫 𝑓)
225 simplrr 777 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))
226 ssralv 3981 . . . . . . . . . . . . . . . . . 18 (𝒫 ⊆ 𝒫 𝑓 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑔𝑑)))
227224, 225, 226sylc 65 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑔𝑑))
228 elpwi 4506 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ 𝒫 𝑑)
229 resima2 5853 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 → ((𝑔) “ 𝑑) = (𝑔𝑑))
230228, 229syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑑 ∈ 𝒫 → ((𝑔) “ 𝑑) = (𝑔𝑑))
231230eqcomd 2804 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ 𝒫 → (𝑔𝑑) = ((𝑔) “ 𝑑))
232231breq2d 5042 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ 𝒫 → (𝑑 ≼ (𝑔𝑑) ↔ 𝑑 ≼ ((𝑔) “ 𝑑)))
233232ralbiia 3132 . . . . . . . . . . . . . . . . 17 (∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑔𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑))
234227, 233sylib 221 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑))
235 imaeq1 5891 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑔) → (𝑐𝑑) = ((𝑔) “ 𝑑))
236235breq2d 5042 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑔) → (𝑑 ≼ (𝑐𝑑) ↔ 𝑑 ≼ ((𝑔) “ 𝑑)))
237236ralbidv 3162 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝑔) → (∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑)))
238 pweq 4513 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑔) → 𝒫 𝑐 = 𝒫 (𝑔))
239238rexeqdv 3365 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝑔) → (∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V))
240237, 239imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑔) → ((∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V)))
241 simpllr 775 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)))
242 psseq1 4015 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = → (𝑎𝑓𝑓))
243 xpeq1 5533 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = → (𝑎 × 𝑏) = ( × 𝑏))
244243pweqd 4516 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = → 𝒫 (𝑎 × 𝑏) = 𝒫 ( × 𝑏))
245 pweq 4513 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = → 𝒫 𝑎 = 𝒫 )
246245raleqdv 3364 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑)))
247 f1eq2 6545 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = → (𝑒:𝑎1-1→V ↔ 𝑒:1-1→V))
248247rexbidv 3256 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V))
249246, 248imbi12d 348 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V)))
250244, 249raleqbidv 3354 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 ( × 𝑏)(∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V)))
251242, 250imbi12d 348 . . . . . . . . . . . . . . . . . . 19 (𝑎 = → ((𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ (𝑓 → ∀𝑐 ∈ 𝒫 ( × 𝑏)(∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V))))
252251spvv 2003 . . . . . . . . . . . . . . . . . 18 (∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) → (𝑓 → ∀𝑐 ∈ 𝒫 ( × 𝑏)(∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V)))
253241, 221, 252sylc 65 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑐 ∈ 𝒫 ( × 𝑏)(∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V))
254 simplrl 776 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → 𝑔 ∈ 𝒫 (𝑓 × 𝑏))
255 ssres 5845 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔) ⊆ ((𝑓 × 𝑏) ↾ ))
256 df-res 5531 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 × 𝑏) ↾ ) = ((𝑓 × 𝑏) ∩ ( × V))
257 inxp 5667 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 × 𝑏) ∩ ( × V)) = ((𝑓) × (𝑏 ∩ V))
258 inss2 4156 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓) ⊆
259 inss1 4155 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 ∩ V) ⊆ 𝑏
260 xpss12 5534 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓) ⊆ ∧ (𝑏 ∩ V) ⊆ 𝑏) → ((𝑓) × (𝑏 ∩ V)) ⊆ ( × 𝑏))
261258, 259, 260mp2an 691 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓) × (𝑏 ∩ V)) ⊆ ( × 𝑏)
262257, 261eqsstri 3949 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 × 𝑏) ∩ ( × V)) ⊆ ( × 𝑏)
263256, 262eqsstri 3949 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 × 𝑏) ↾ ) ⊆ ( × 𝑏)
264255, 263sstrdi 3927 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔) ⊆ ( × 𝑏))
26594, 264syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔) ⊆ ( × 𝑏))
26645resex 5866 . . . . . . . . . . . . . . . . . . . 20 (𝑔) ∈ V
267266elpw 4501 . . . . . . . . . . . . . . . . . . 19 ((𝑔) ∈ 𝒫 ( × 𝑏) ↔ (𝑔) ⊆ ( × 𝑏))
268265, 267sylibr 237 . . . . . . . . . . . . . . . . . 18 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔) ∈ 𝒫 ( × 𝑏))
269254, 268syl 17 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (𝑔) ∈ 𝒫 ( × 𝑏))
270240, 253, 269rspcdva 3573 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V))
271234, 270mpd 15 . . . . . . . . . . . . . . 15 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V)
272 f1eq1 6544 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑖 → (𝑒:1-1→V ↔ 𝑖:1-1→V))
273272cbvrexvw 3397 . . . . . . . . . . . . . . 15 (∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V ↔ ∃𝑖 ∈ 𝒫 (𝑔)𝑖:1-1→V)
274271, 273sylib 221 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑖 ∈ 𝒫 (𝑔)𝑖:1-1→V)
275 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑐) → 𝑑 = (𝑐))
276 imaeq2 5892 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑐) → (𝑔𝑑) = (𝑔 “ (𝑐)))
277275, 276breq12d 5043 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = (𝑐) → (𝑑 ≼ (𝑔𝑑) ↔ (𝑐) ≼ (𝑔 “ (𝑐))))
278 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))
279278ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))
280222ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔)) → 𝑓)
281280ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑓)
282 elpwi 4506 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ 𝒫 (𝑓) → 𝑐 ⊆ (𝑓))
283 difss 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓) ⊆ 𝑓
284282, 283sstrdi 3927 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ 𝒫 (𝑓) → 𝑐𝑓)
285284adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑐𝑓)
286281, 285unssd 4113 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) ⊆ 𝑓)
287128elpw2 5212 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐) ∈ 𝒫 𝑓 ↔ (𝑐) ⊆ 𝑓)
288286, 287sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) ∈ 𝒫 𝑓)
289277, 279, 288rspcdva 3573 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) ≼ (𝑔 “ (𝑐)))
290 imaundi 5975 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 “ (𝑐)) = ((𝑔) ∪ (𝑔𝑐))
291 undif2 4383 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔))) = ((𝑔) ∪ (𝑔𝑐))
292290, 291eqtr4i 2824 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 “ (𝑐)) = ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔)))
293289, 292breqtrdi 5071 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) ≼ ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔))))
294 simp-4l 782 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑓 ∈ Fin)
295294, 281ssfid 8725 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ∈ Fin)
296 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = 𝑑 = )
297 imaeq2 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = → (𝑔𝑑) = (𝑔))
298296, 297breq12d 5043 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = → (𝑑 ≼ (𝑔𝑑) ↔ ≼ (𝑔)))
299 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ∈ V
300299elpw 4501 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ 𝒫 𝑓𝑓)
301281, 300sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ∈ 𝒫 𝑓)
302298, 279, 301rspcdva 3573 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ≼ (𝑔))
303 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ¬ ≺ (𝑔))
304 bren2 8523 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( ≈ (𝑔) ↔ ( ≼ (𝑔) ∧ ¬ ≺ (𝑔)))
305302, 303, 304sylanbrc 586 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ≈ (𝑔))
306305ensymd 8543 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑔) ≈ )
307 incom 4128 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐) = (𝑐)
308 ssdifin0 4389 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 ⊆ (𝑓) → (𝑐) = ∅)
309307, 308syl5eq 2845 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 ⊆ (𝑓) → (𝑐) = ∅)
310282, 309syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 ∈ 𝒫 (𝑓) → (𝑐) = ∅)
311310adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) = ∅)
312 disjdif 4379 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔) ∩ ((𝑔𝑐) ∖ (𝑔))) = ∅
313312a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ((𝑔) ∩ ((𝑔𝑐) ∖ (𝑔))) = ∅)
314 domunfican 8775 . . . . . . . . . . . . . . . . . . . . . . 23 ((( ∈ Fin ∧ (𝑔) ≈ ) ∧ ((𝑐) = ∅ ∧ ((𝑔) ∩ ((𝑔𝑐) ∖ (𝑔))) = ∅)) → ((𝑐) ≼ ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔))) ↔ 𝑐 ≼ ((𝑔𝑐) ∖ (𝑔))))
315295, 306, 311, 313, 314syl22anc 837 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ((𝑐) ≼ ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔))) ↔ 𝑐 ≼ ((𝑔𝑐) ∖ (𝑔))))
316293, 315mpbid 235 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑐 ≼ ((𝑔𝑐) ∖ (𝑔)))
317101difeq1d 4049 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)) = ((𝑔𝑐) ∖ (𝑔)))
318317ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)) = ((𝑔𝑐) ∖ (𝑔)))
319318ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)) = ((𝑔𝑐) ∖ (𝑔)))
320316, 319breqtrrd 5058 . . . . . . . . . . . . . . . . . . . 20 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑐 ≼ (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)))
321 df-ss 3898 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 ⊆ (𝑓) ↔ (𝑐 ∩ (𝑓)) = 𝑐)
322282, 321sylib 221 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 ∈ 𝒫 (𝑓) → (𝑐 ∩ (𝑓)) = 𝑐)
323322imaeq2d 5896 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 ∈ 𝒫 (𝑓) → (𝑔 “ (𝑐 ∩ (𝑓))) = (𝑔𝑐))
324323ineq1d 4138 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ 𝒫 (𝑓) → ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) = ((𝑔𝑐) ∩ (𝑏 ∖ (𝑔))))
325 indif2 4197 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔𝑐) ∩ (𝑏 ∖ (𝑔))) = (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔))
326324, 325eqtrdi 2849 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 ∈ 𝒫 (𝑓) → ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) = (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)))
327326adantl 485 . . . . . . . . . . . . . . . . . . . 20 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) = (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)))
328320, 327breqtrrd 5058 . . . . . . . . . . . . . . . . . . 19 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))))
329328ralrimiva 3149 . . . . . . . . . . . . . . . . . 18 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑐 ∈ 𝒫 (𝑓)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))))
330 imainrect 6005 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔)))
331 imaeq2 5892 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑐) = ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
332330, 331syl5eqr 2847 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) = ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
333109, 332breq12d 5043 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑)))
334333cbvralvw 3396 . . . . . . . . . . . . . . . . . 18 (∀𝑐 ∈ 𝒫 (𝑓)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) ↔ ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
335329, 334sylib 221 . . . . . . . . . . . . . . . . 17 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
336335adantllr 718 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
337 inss2 4156 . . . . . . . . . . . . . . . . . . 19 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ⊆ ((𝑓) × (𝑏 ∖ (𝑔)))
338 difss 4059 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∖ (𝑔)) ⊆ 𝑏
339 xpss2 5539 . . . . . . . . . . . . . . . . . . . 20 ((𝑏 ∖ (𝑔)) ⊆ 𝑏 → ((𝑓) × (𝑏 ∖ (𝑔))) ⊆ ((𝑓) × 𝑏))
340338, 339ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑓) × (𝑏 ∖ (𝑔))) ⊆ ((𝑓) × 𝑏)
341337, 340sstri 3924 . . . . . . . . . . . . . . . . . 18 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ⊆ ((𝑓) × 𝑏)
34245inex1 5185 . . . . . . . . . . . . . . . . . . 19 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∈ V
343342elpw 4501 . . . . . . . . . . . . . . . . . 18 ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∈ 𝒫 ((𝑓) × 𝑏) ↔ (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ⊆ ((𝑓) × 𝑏))
344341, 343mpbir 234 . . . . . . . . . . . . . . . . 17 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∈ 𝒫 ((𝑓) × 𝑏)
345 incom 4128 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓) = (𝑓)
346 df-ss 3898 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 ↔ (𝑓) = )
347222, 346sylib 221 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 → (𝑓) = )
348345, 347syl5eq 2845 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 → (𝑓) = )
349348neeq1d 3046 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 → ((𝑓) ≠ ∅ ↔ ≠ ∅))
350349biimpar 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ≠ ∅) → (𝑓) ≠ ∅)
351 disj4 4366 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓) = ∅ ↔ ¬ (𝑓) ⊊ 𝑓)
352351bicomi 227 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑓) ⊊ 𝑓 ↔ (𝑓) = ∅)
353352necon1abii 3035 . . . . . . . . . . . . . . . . . . . 20 ((𝑓) ≠ ∅ ↔ (𝑓) ⊊ 𝑓)
354350, 353sylib 221 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ≠ ∅) → (𝑓) ⊊ 𝑓)
355354ad2antrl 727 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (𝑓) ⊊ 𝑓)
356128difexi 5196 . . . . . . . . . . . . . . . . . . 19 (𝑓) ∈ V
357 psseq1 4015 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑓) → (𝑎𝑓 ↔ (𝑓) ⊊ 𝑓))
358 xpeq1 5533 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑓) → (𝑎 × 𝑏) = ((𝑓) × 𝑏))
359358pweqd 4516 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑓) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓) × 𝑏))
360 pweq 4513 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑓) → 𝒫 𝑎 = 𝒫 (𝑓))
361360raleqdv 3364 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑓) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑)))
362 f1eq2 6545 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑓) → (𝑒:𝑎1-1→V ↔ 𝑒:(𝑓)–1-1→V))
363362rexbidv 3256 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑓) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V))
364361, 363imbi12d 348 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑓) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V)))
365359, 364raleqbidv 3354 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑓) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V)))
366357, 365imbi12d 348 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑓) → ((𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ ((𝑓) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V))))
367356, 366spcv 3554 . . . . . . . . . . . . . . . . . 18 (∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) → ((𝑓) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V)))
368241, 355, 367sylc 65 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V))
369 imaeq1 5891 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → (𝑐𝑑) = ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
370369breq2d 5042 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → (𝑑 ≼ (𝑐𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑)))
371370ralbidv 3162 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑)))
372 pweq 4513 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))))
373372rexeqdv 3365 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V))
374371, 373imbi12d 348 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → ((∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V)))
375374rspcva 3569 . . . . . . . . . . . . . . . . 17 (((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∈ 𝒫 ((𝑓) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V))
376344, 368, 375sylancr 590 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V))
377336, 376mpd 15 . . . . . . . . . . . . . . 15 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V)
378 f1eq1 6544 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑗 → (𝑒:(𝑓)–1-1→V ↔ 𝑗:(𝑓)–1-1→V))
379378cbvrexvw 3397 . . . . . . . . . . . . . . 15 (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V ↔ ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V)
380377, 379sylib 221 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V)
381 elpwi 4506 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ 𝒫 (𝑔) → 𝑖 ⊆ (𝑔))
382 resss 5843 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔) ⊆ 𝑔
383381, 382sstrdi 3927 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ 𝒫 (𝑔) → 𝑖𝑔)
384383adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V) → 𝑖𝑔)
385384ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → 𝑖𝑔)
386 elpwi 4506 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → 𝑗 ⊆ (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))))
387 inss1 4155 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ⊆ 𝑔
388386, 387sstrdi 3927 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → 𝑗𝑔)
389388ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → 𝑗𝑔)
390385, 389unssd 4113 . . . . . . . . . . . . . . . . . . 19 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗) ⊆ 𝑔)
39145elpw2 5212 . . . . . . . . . . . . . . . . . . 19 ((𝑖𝑗) ∈ 𝒫 𝑔 ↔ (𝑖𝑗) ⊆ 𝑔)
392390, 391sylibr 237 . . . . . . . . . . . . . . . . . 18 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗) ∈ 𝒫 𝑔)
393 f1f1orn 6601 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖:1-1→V → 𝑖:1-1-onto→ran 𝑖)
394393adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V) → 𝑖:1-1-onto→ran 𝑖)
395394ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → 𝑖:1-1-onto→ran 𝑖)
396 f1f1orn 6601 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗:(𝑓)–1-1→V → 𝑗:(𝑓)–1-1-onto→ran 𝑗)
397396ad2antll 728 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → 𝑗:(𝑓)–1-1-onto→ran 𝑗)
398 disjdif 4379 . . . . . . . . . . . . . . . . . . . . . . 23 ( ∩ (𝑓)) = ∅
399398a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ( ∩ (𝑓)) = ∅)
400 rnss 5773 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ⊆ (𝑔) → ran 𝑖 ⊆ ran (𝑔))
401381, 400syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ 𝒫 (𝑔) → ran 𝑖 ⊆ ran (𝑔))
402 df-ima 5532 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔) = ran (𝑔)
403401, 402sseqtrrdi 3966 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ 𝒫 (𝑔) → ran 𝑖 ⊆ (𝑔))
404403adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V) → ran 𝑖 ⊆ (𝑔))
405404ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ran 𝑖 ⊆ (𝑔))
406 incom 4128 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔) ∩ ran 𝑗) = (ran 𝑗 ∩ (𝑔))
407386, 337sstrdi 3927 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → 𝑗 ⊆ ((𝑓) × (𝑏 ∖ (𝑔))))
408 rnss 5773 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ⊆ ((𝑓) × (𝑏 ∖ (𝑔))) → ran 𝑗 ⊆ ran ((𝑓) × (𝑏 ∖ (𝑔))))
409407, 408syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → ran 𝑗 ⊆ ran ((𝑓) × (𝑏 ∖ (𝑔))))
410 rnxpss 5996 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ran ((𝑓) × (𝑏 ∖ (𝑔))) ⊆ (𝑏 ∖ (𝑔))
411409, 410sstrdi 3927 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔)))
412411ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔)))
413 incom 4128 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏 ∖ (𝑔)) ∩ (𝑔)) = ((𝑔) ∩ (𝑏 ∖ (𝑔)))
414 disjdif 4379 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔) ∩ (𝑏 ∖ (𝑔))) = ∅
415413, 414eqtri 2821 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 ∖ (𝑔)) ∩ (𝑔)) = ∅
416 ssdisj 4367 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ran 𝑗 ⊆ (𝑏 ∖ (𝑔)) ∧ ((𝑏 ∖ (𝑔)) ∩ (𝑔)) = ∅) → (ran 𝑗 ∩ (𝑔)) = ∅)
417412, 415, 416sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (ran 𝑗 ∩ (𝑔)) = ∅)
418406, 417syl5eq 2845 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ((𝑔) ∩ ran 𝑗) = ∅)
419 ssdisj 4367 . . . . . . . . . . . . . . . . . . . . . . 23 ((ran 𝑖 ⊆ (𝑔) ∧ ((𝑔) ∩ ran 𝑗) = ∅) → (ran 𝑖 ∩ ran 𝑗) = ∅)
420405, 418, 419syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (ran 𝑖 ∩ ran 𝑗) = ∅)
421 f1oun 6609 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑖:1-1-onto→ran 𝑖𝑗:(𝑓)–1-1-onto→ran 𝑗) ∧ (( ∩ (𝑓)) = ∅ ∧ (ran 𝑖 ∩ ran 𝑗) = ∅)) → (𝑖𝑗):( ∪ (𝑓))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
422395, 397, 399, 420, 421syl22anc 837 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗):( ∪ (𝑓))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
423 undif 4388 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 ↔ ( ∪ (𝑓)) = 𝑓)
424423biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 → ( ∪ (𝑓)) = 𝑓)
425424adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) → ( ∪ (𝑓)) = 𝑓)
426425ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ( ∪ (𝑓)) = 𝑓)
427426f1oeq2d 6586 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ((𝑖𝑗):( ∪ (𝑓))–1-1-onto→(ran 𝑖 ∪ ran 𝑗) ↔ (𝑖𝑗):𝑓1-1-onto→(ran 𝑖 ∪ ran 𝑗)))
428422, 427mpbid 235 . . . . . . . . . . . . . . . . . . . 20 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗):𝑓1-1-onto→(ran 𝑖 ∪ ran 𝑗))
429 f1of1 6589 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑗):𝑓1-1-onto→(ran 𝑖 ∪ ran 𝑗) → (𝑖𝑗):𝑓1-1→(ran 𝑖 ∪ ran 𝑗))
430428, 429syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗):𝑓1-1→(ran 𝑖 ∪ ran 𝑗))
431 ssv 3939 . . . . . . . . . . . . . . . . . . 19 (ran 𝑖 ∪ ran 𝑗) ⊆ V
432 f1ss 6555 . . . . . . . . . . . . . . . . . . 19 (((𝑖𝑗):𝑓1-1→(ran 𝑖 ∪ ran 𝑗) ∧ (ran 𝑖 ∪ ran 𝑗) ⊆ V) → (𝑖𝑗):𝑓1-1→V)
433430, 431, 432sylancl 589 . . . . . . . . . . . . . . . . . 18 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗):𝑓1-1→V)
434 f1eq1 6544 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑖𝑗) → (𝑒:𝑓1-1→V ↔ (𝑖𝑗):𝑓1-1→V))
435434rspcev 3571 . . . . . . . . . . . . . . . . . 18 (((𝑖𝑗) ∈ 𝒫 𝑔 ∧ (𝑖𝑗):𝑓1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
436392, 433, 435syl2anc 587 . . . . . . . . . . . . . . . . 17 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
437436rexlimdvaa 3244 . . . . . . . . . . . . . . . 16 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
438437rexlimdvaa 3244 . . . . . . . . . . . . . . 15 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) → (∃𝑖 ∈ 𝒫 (𝑔)𝑖:1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
439254, 223, 438syl2anc 587 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (∃𝑖 ∈ 𝒫 (𝑔)𝑖:1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
440274, 380, 439mp2d 49 . . . . . . . . . . . . 13 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
441440ex 416 . . . . . . . . . . . 12 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → (((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
442441exlimdv 1934 . . . . . . . . . . 11 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → (∃((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
443442imp 410 . . . . . . . . . 10 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∃((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
444220, 443sylan2br 597 . . . . . . . . 9 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ¬ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
445219, 444pm2.61dan 812 . . . . . . . 8 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
446445exp32 424 . . . . . . 7 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
447446ralrimiv 3148 . . . . . 6 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → ∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
448 imaeq1 5891 . . . . . . . . . 10 (𝑔 = 𝑐 → (𝑔𝑑) = (𝑐𝑑))
449448breq2d 5042 . . . . . . . . 9 (𝑔 = 𝑐 → (𝑑 ≼ (𝑔𝑑) ↔ 𝑑 ≼ (𝑐𝑑)))
450449ralbidv 3162 . . . . . . . 8 (𝑔 = 𝑐 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑)))
451 pweq 4513 . . . . . . . . 9 (𝑔 = 𝑐 → 𝒫 𝑔 = 𝒫 𝑐)
452451rexeqdv 3365 . . . . . . . 8 (𝑔 = 𝑐 → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))
453450, 452imbi12d 348 . . . . . . 7 (𝑔 = 𝑐 → ((∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V)))
454453cbvralvw 3396 . . . . . 6 (∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))
455447, 454sylib 221 . . . . 5 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))
456455exp31 423 . . . 4 (𝑓 ∈ Fin → (𝑏 ∈ Fin → (∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))))
457456a2d 29 . . 3 (𝑓 ∈ Fin → ((𝑏 ∈ Fin → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))))
45822, 457syl5bi 245 . 2 (𝑓 ∈ Fin → (∀𝑎(𝑎𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))))
4599, 18, 458findcard3 8745 1 (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wal 1536   = wceq 1538  wex 1781  wcel 2111  wne 2987  wral 3106  wrex 3107  Vcvv 3441  cdif 3878  cun 3879  cin 3880  wss 3881  wpss 3882  c0 4243  𝒫 cpw 4497  {csn 4525  cop 4531   class class class wbr 5030   × cxp 5517  ran crn 5520  cres 5521  cima 5522  1-1wf1 6321  1-1-ontowf1o 6323  cen 8489  cdom 8490  csdm 8491  Fincfn 8492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-om 7561  df-1o 8085  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496
This theorem is referenced by:  marypha1  8882
  Copyright terms: Public domain W3C validator