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

Theorem marypha1lem 8096
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 4946 . . . . 5 (𝑎 = 𝑓 → (𝑎 × 𝑏) = (𝑓 × 𝑏))
21pweqd 4016 . . . 4 (𝑎 = 𝑓 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝑓 × 𝑏))
3 pweq 4014 . . . . . 6 (𝑎 = 𝑓 → 𝒫 𝑎 = 𝒫 𝑓)
43raleqdv 3025 . . . . 5 (𝑎 = 𝑓 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑)))
5 f1eq2 5893 . . . . . 6 (𝑎 = 𝑓 → (𝑒:𝑎1-1→V ↔ 𝑒:𝑓1-1→V))
65rexbidv 2938 . . . . 5 (𝑎 = 𝑓 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))
74, 6imbi12d 332 . . . 4 (𝑎 = 𝑓 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V)))
82, 7raleqbidv 3033 . . 3 (𝑎 = 𝑓 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V)))
98imbi2d 328 . 2 (𝑎 = 𝑓 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))))
10 xpeq1 4946 . . . . 5 (𝑎 = 𝐴 → (𝑎 × 𝑏) = (𝐴 × 𝑏))
1110pweqd 4016 . . . 4 (𝑎 = 𝐴 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝐴 × 𝑏))
12 pweq 4014 . . . . . 6 (𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴)
1312raleqdv 3025 . . . . 5 (𝑎 = 𝐴 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑)))
14 f1eq2 5893 . . . . . 6 (𝑎 = 𝐴 → (𝑒:𝑎1-1→V ↔ 𝑒:𝐴1-1→V))
1514rexbidv 2938 . . . . 5 (𝑎 = 𝐴 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V))
1613, 15imbi12d 332 . . . 4 (𝑎 = 𝐴 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V)))
1711, 16raleqbidv 3033 . . 3 (𝑎 = 𝐴 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V)))
1817imbi2d 328 . 2 (𝑎 = 𝐴 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V))))
19 bi2.04 374 . . . . 5 ((𝑎𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ↔ (𝑏 ∈ Fin → (𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))))
2019albii 1722 . . . 4 (∀𝑎(𝑎𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ↔ ∀𝑎(𝑏 ∈ Fin → (𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))))
21 19.21v 1821 . . . 4 (∀𝑎(𝑏 ∈ Fin → (𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))))
2220, 21bitri 262 . . 3 (∀𝑎(𝑎𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))))
23 0elpw 4659 . . . . . . . . . . . . 13 ∅ ∈ 𝒫 𝑔
24 f10 5964 . . . . . . . . . . . . 13 ∅:∅–1-1→V
25 f1eq1 5892 . . . . . . . . . . . . . 14 (𝑒 = ∅ → (𝑒:∅–1-1→V ↔ ∅:∅–1-1→V))
2625rspcev 3186 . . . . . . . . . . . . 13 ((∅ ∈ 𝒫 𝑔 ∧ ∅:∅–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V)
2723, 24, 26mp2an 703 . . . . . . . . . . . 12 𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V
28 f1eq2 5893 . . . . . . . . . . . . 13 (𝑓 = ∅ → (𝑒:𝑓1-1→V ↔ 𝑒:∅–1-1→V))
2928rexbidv 2938 . . . . . . . . . . . 12 (𝑓 = ∅ → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V))
3027, 29mpbiri 246 . . . . . . . . . . 11 (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
3130a1i 11 . . . . . . . . . 10 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
32 n0 3793 . . . . . . . . . . 11 (𝑓 ≠ ∅ ↔ ∃𝑖 𝑖𝑓)
33 snelpwi 4738 . . . . . . . . . . . . . . . . . . 19 (𝑖𝑓 → {𝑖} ∈ 𝒫 𝑓)
34 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = {𝑖} → 𝑑 = {𝑖})
35 imaeq2 5271 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = {𝑖} → (𝑔𝑑) = (𝑔 “ {𝑖}))
3634, 35breq12d 4494 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 = {𝑖} → (𝑑 ≼ (𝑔𝑑) ↔ {𝑖} ≼ (𝑔 “ {𝑖})))
3736rspcva 3184 . . . . . . . . . . . . . . . . . . . . 21 (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → {𝑖} ≼ (𝑔 “ {𝑖}))
38 vex 3080 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑖 ∈ V
3938snnz 4155 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑖} ≠ ∅
40 snex 4734 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑖} ∈ V
41400sdom 7850 . . . . . . . . . . . . . . . . . . . . . . . 24 (∅ ≺ {𝑖} ↔ {𝑖} ≠ ∅)
4239, 41mpbir 219 . . . . . . . . . . . . . . . . . . . . . . 23 ∅ ≺ {𝑖}
43 sdomdomtr 7852 . . . . . . . . . . . . . . . . . . . . . . 23 ((∅ ≺ {𝑖} ∧ {𝑖} ≼ (𝑔 “ {𝑖})) → ∅ ≺ (𝑔 “ {𝑖}))
4442, 43mpan 701 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑖} ≼ (𝑔 “ {𝑖}) → ∅ ≺ (𝑔 “ {𝑖}))
45 vex 3080 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑔 ∈ V
46 imaexg 6869 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 ∈ V → (𝑔 “ {𝑖}) ∈ V)
4745, 46ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 “ {𝑖}) ∈ V
48470sdom 7850 . . . . . . . . . . . . . . . . . . . . . 22 (∅ ≺ (𝑔 “ {𝑖}) ↔ (𝑔 “ {𝑖}) ≠ ∅)
4944, 48sylib 206 . . . . . . . . . . . . . . . . . . . . 21 ({𝑖} ≼ (𝑔 “ {𝑖}) → (𝑔 “ {𝑖}) ≠ ∅)
5037, 49syl 17 . . . . . . . . . . . . . . . . . . . 20 (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → (𝑔 “ {𝑖}) ≠ ∅)
5150expcom 449 . . . . . . . . . . . . . . . . . . 19 (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ({𝑖} ∈ 𝒫 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
5233, 51syl5 33 . . . . . . . . . . . . . . . . . 18 (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → (𝑖𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
5352adantl 480 . . . . . . . . . . . . . . . . 17 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → (𝑖𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
5453ad2antlr 758 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑖𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
5554impr 646 . . . . . . . . . . . . . . 15 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → (𝑔 “ {𝑖}) ≠ ∅)
56 n0 3793 . . . . . . . . . . . . . . 15 ((𝑔 “ {𝑖}) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
5755, 56sylib 206 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
58 imaexg 6869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔 ∈ V → (𝑔𝑐) ∈ V)
59 difexg 4634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑔𝑐) ∈ V → ((𝑔𝑐) ∖ {𝑗}) ∈ V)
6045, 58, 59mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔𝑐) ∖ {𝑗}) ∈ V
61600dom 7849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ ≼ ((𝑔𝑐) ∖ {𝑗})
62 breq1 4484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = ∅ → (𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}) ↔ ∅ ≼ ((𝑔𝑐) ∖ {𝑗})))
6361, 62mpbiri 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = ∅ → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
6463a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 = ∅ → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗})))
65 simpll 785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → ∀((𝑓 ≠ ∅) → ≺ (𝑔)))
66 elpwi 4020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
6766ad2antrl 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
68 difsnpss 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓)
6968biimpi 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖𝑓 → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
7069ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
7167, 70sspsstrd 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐𝑓)
72 simprr 791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≠ ∅)
7371, 72jca 552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑐𝑓𝑐 ≠ ∅))
74 psseq1 3560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑐 → (𝑓𝑐𝑓))
75 neeq1 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑐 → ( ≠ ∅ ↔ 𝑐 ≠ ∅))
7674, 75anbi12d 742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( = 𝑐 → ((𝑓 ≠ ∅) ↔ (𝑐𝑓𝑐 ≠ ∅)))
77 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑐 = 𝑐)
78 imaeq2 5271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑐 → (𝑔) = (𝑔𝑐))
7977, 78breq12d 4494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( = 𝑐 → ( ≺ (𝑔) ↔ 𝑐 ≺ (𝑔𝑐)))
8076, 79imbi12d 332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ( = 𝑐 → (((𝑓 ≠ ∅) → ≺ (𝑔)) ↔ ((𝑐𝑓𝑐 ≠ ∅) → 𝑐 ≺ (𝑔𝑐))))
8180spv 2151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀((𝑓 ≠ ∅) → ≺ (𝑔)) → ((𝑐𝑓𝑐 ≠ ∅) → 𝑐 ≺ (𝑔𝑐)))
8265, 73, 81sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≺ (𝑔𝑐))
83 domdifsn 7802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ≺ (𝑔𝑐) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
8482, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
8584expr 640 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 ≠ ∅ → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗})))
8664, 85pm2.61dne 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
8786adantlrr 752 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
8887adantll 745 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔𝑐) ∖ {𝑗}))
89 df-ss 3458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ⊆ (𝑓 ∖ {𝑖}) ↔ (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
9066, 89sylib 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
9190imaeq2d 5275 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) = (𝑔𝑐))
9291ineq1d 3678 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})))
9392adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})))
94 indif2 3732 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})) = (((𝑔𝑐) ∩ 𝑏) ∖ {𝑗})
95 imassrn 5286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔𝑐) ⊆ ran 𝑔
96 elpwi 4020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → 𝑔 ⊆ (𝑓 × 𝑏))
97 rnss 5166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔 ⊆ ran (𝑓 × 𝑏))
98 rnxpss 5375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ran (𝑓 × 𝑏) ⊆ 𝑏
9997, 98syl6ss 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔𝑏)
10096, 99syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ran 𝑔𝑏)
10195, 100syl5ss 3483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔𝑐) ⊆ 𝑏)
102 df-ss 3458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔𝑐) ⊆ 𝑏 ↔ ((𝑔𝑐) ∩ 𝑏) = (𝑔𝑐))
103101, 102sylib 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑔𝑐) ∩ 𝑏) = (𝑔𝑐))
104103difeq1d 3593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔𝑐) ∖ {𝑗}))
105104ad2antrl 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → (((𝑔𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔𝑐) ∖ {𝑗}))
10694, 105syl5eq 2560 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∖ {𝑗}))
107106ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∖ {𝑗}))
10893, 107eqtrd 2548 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔𝑐) ∖ {𝑗}))
10988, 108breqtrrd 4509 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
110109ralrimiva 2853 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
111 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑑𝑐 = 𝑑)
112 imainrect 5384 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗}))
113 imaeq2 5271 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
114112, 113syl5eqr 2562 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
115111, 114breq12d 4494 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
116115cbvralv 3051 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
117110, 116sylib 206 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
118117adantllr 750 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
119 inss2 3699 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))
120 difss 3603 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 ∖ {𝑗}) ⊆ 𝑏
121 xpss2 5045 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 ∖ {𝑗}) ⊆ 𝑏 → ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
122120, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
123119, 122sstri 3481 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
12445inex1 4626 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ V
125124elpw 4017 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ↔ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
126123, 125mpbir 219 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)
127 simpllr 794 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)))
12869adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
129128ad2antll 760 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
130 vex 3080 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑓 ∈ V
131 difexg 4634 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 ∈ V → (𝑓 ∖ {𝑖}) ∈ V)
132130, 131ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 ∖ {𝑖}) ∈ V
133 psseq1 3560 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓))
134 xpeq1 4946 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎 × 𝑏) = ((𝑓 ∖ {𝑖}) × 𝑏))
135134pweqd 4016 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏))
136 pweq 4014 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 𝑎 = 𝒫 (𝑓 ∖ {𝑖}))
137136raleqdv 3025 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑)))
138 f1eq2 5893 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = (𝑓 ∖ {𝑖}) → (𝑒:𝑎1-1→V ↔ 𝑒:(𝑓 ∖ {𝑖})–1-1→V))
139138rexbidv 2938 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝑓 ∖ {𝑖}) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
140137, 139imbi12d 332 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (𝑓 ∖ {𝑖}) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
141135, 140raleqbidv 3033 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
142133, 141imbi12d 332 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑓 ∖ {𝑖}) → ((𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))))
143132, 142spcv 3176 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) → ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
144127, 129, 143sylc 62 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
145 imaeq1 5270 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑐𝑑) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
146145breq2d 4493 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑑 ≼ (𝑐𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
147146ralbidv 2873 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
148 pweq 4014 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
149148rexeqdv 3026 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
150147, 149imbi12d 332 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ((∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
151150rspcva 3184 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
152126, 144, 151sylancr 693 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
153118, 152mpd 15 . . . . . . . . . . . . . . . . . . . 20 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)
154 f1eq1 5892 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = 𝑘 → (𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ 𝑘:(𝑓 ∖ {𝑖})–1-1→V))
155154cbvrexv 3052 . . . . . . . . . . . . . . . . . . . 20 (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
156153, 155sylib 206 . . . . . . . . . . . . . . . . . . 19 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
157 vex 3080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑗 ∈ V
15838, 157elimasn 5300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (𝑔 “ {𝑖}) ↔ ⟨𝑖, 𝑗⟩ ∈ 𝑔)
159158biimpi 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (𝑔 “ {𝑖}) → ⟨𝑖, 𝑗⟩ ∈ 𝑔)
160159snssd 4184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (𝑔 “ {𝑖}) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
161160ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
162 elpwi 4020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
163 inss1 3698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ 𝑔
164162, 163syl6ss 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘𝑔)
165164adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → 𝑘𝑔)
166161, 165unssd 3655 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
16745elpw2 4654 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
168166, 167sylibr 222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
169168ad2ant2lr 779 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
17038, 157f1osn 5971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗}
171170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗})
172 f1f1orn 5944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘:(𝑓 ∖ {𝑖})–1-1→V → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
173172adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
174 disjdif 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅
175174a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅)
176 incom 3670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ({𝑗} ∩ ran 𝑘) = (ran 𝑘 ∩ {𝑗})
177162, 119syl6ss 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
178 rnss 5166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
179 rnxpss 5375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ (𝑏 ∖ {𝑗})
180178, 179syl6ss 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
181177, 180syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
182 incom 3670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ({𝑗} ∩ (𝑏 ∖ {𝑗}))
183 disjdif 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ({𝑗} ∩ (𝑏 ∖ {𝑗})) = ∅
184182, 183eqtri 2536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅
185 ssdisj 3881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((ran 𝑘 ⊆ (𝑏 ∖ {𝑗}) ∧ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅) → (ran 𝑘 ∩ {𝑗}) = ∅)
186181, 184, 185sylancl 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (ran 𝑘 ∩ {𝑗}) = ∅)
187176, 186syl5eq 2560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ({𝑗} ∩ ran 𝑘) = ∅)
188187adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑗} ∩ ran 𝑘) = ∅)
189 f1oun 5952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((({⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗} ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘) ∧ (({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅ ∧ ({𝑗} ∩ ran 𝑘) = ∅)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
190171, 173, 175, 188, 189syl22anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
191190adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
192 snssi 4183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖𝑓 → {𝑖} ⊆ 𝑓)
193192ad2antrl 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) → {𝑖} ⊆ 𝑓)
194 undif 3904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ({𝑖} ⊆ 𝑓 ↔ ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
195193, 194sylib 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) → ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
196 f1oeq2 5924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓 → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘)))
197195, 196syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘)))
198197adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘)))
199191, 198mpbid 220 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘))
200 f1of1 5932 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→({𝑗} ∪ ran 𝑘))
201 ssv 3492 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({𝑗} ∪ ran 𝑘) ⊆ V
202 f1ss 5902 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→({𝑗} ∪ ran 𝑘) ∧ ({𝑗} ∪ ran 𝑘) ⊆ V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V)
203200, 201, 202sylancl 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V)
204199, 203syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V)
205 f1eq1 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑒 = ({⟨𝑖, 𝑗⟩} ∪ 𝑘) → (𝑒:𝑓1-1→V ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V))
206205rspcev 3186 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ∧ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
207169, 204, 206syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
208207rexlimdvaa 2918 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖}))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
209208ex 448 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
210209adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
211210ad2antlr 758 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
212211impr 646 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
213212adantllr 750 . . . . . . . . . . . . . . . . . . 19 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
214156, 213mpd 15 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ (𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
215214expr 640 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → ((𝑖𝑓𝑗 ∈ (𝑔 “ {𝑖})) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
216215expd 450 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑖𝑓 → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
217216impr 646 . . . . . . . . . . . . . . 15 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
218217exlimdv 1814 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → (∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
21957, 218mpd 15 . . . . . . . . . . . . 13 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ (∀((𝑓 ≠ ∅) → ≺ (𝑔)) ∧ 𝑖𝑓)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
220219expr 640 . . . . . . . . . . . 12 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑖𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
221220exlimdv 1814 . . . . . . . . . . 11 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (∃𝑖 𝑖𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
22232, 221syl5bi 230 . . . . . . . . . 10 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → (𝑓 ≠ ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
22331, 222pm2.61dne 2772 . . . . . . . . 9 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
224 exanali 1755 . . . . . . . . . 10 (∃((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔)) ↔ ¬ ∀((𝑓 ≠ ∅) → ≺ (𝑔)))
225 simprll 797 . . . . . . . . . . . . . . . . . . . 20 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → 𝑓)
226 pssss 3568 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑓)
227225, 226syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → 𝑓)
228 sspwb 4742 . . . . . . . . . . . . . . . . . . 19 (𝑓 ↔ 𝒫 ⊆ 𝒫 𝑓)
229227, 228sylib 206 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → 𝒫 ⊆ 𝒫 𝑓)
230 simplrr 796 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))
231 ssralv 3533 . . . . . . . . . . . . . . . . . 18 (𝒫 ⊆ 𝒫 𝑓 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑔𝑑)))
232229, 230, 231sylc 62 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑔𝑑))
233 elpwi 4020 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ 𝒫 𝑑)
234 resima2 5243 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 → ((𝑔) “ 𝑑) = (𝑔𝑑))
235233, 234syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑑 ∈ 𝒫 → ((𝑔) “ 𝑑) = (𝑔𝑑))
236235eqcomd 2520 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ 𝒫 → (𝑔𝑑) = ((𝑔) “ 𝑑))
237236breq2d 4493 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ 𝒫 → (𝑑 ≼ (𝑔𝑑) ↔ 𝑑 ≼ ((𝑔) “ 𝑑)))
238237ralbiia 2866 . . . . . . . . . . . . . . . . 17 (∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑔𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑))
239232, 238sylib 206 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑))
240 simplrl 795 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → 𝑔 ∈ 𝒫 (𝑓 × 𝑏))
241 ssres 5235 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔) ⊆ ((𝑓 × 𝑏) ↾ ))
242 df-res 4944 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 × 𝑏) ↾ ) = ((𝑓 × 𝑏) ∩ ( × V))
243 inxp 5068 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 × 𝑏) ∩ ( × V)) = ((𝑓) × (𝑏 ∩ V))
244 inss2 3699 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓) ⊆
245 inss1 3698 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 ∩ V) ⊆ 𝑏
246 xpss12 5041 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓) ⊆ ∧ (𝑏 ∩ V) ⊆ 𝑏) → ((𝑓) × (𝑏 ∩ V)) ⊆ ( × 𝑏))
247244, 245, 246mp2an 703 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓) × (𝑏 ∩ V)) ⊆ ( × 𝑏)
248243, 247eqsstri 3502 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 × 𝑏) ∩ ( × V)) ⊆ ( × 𝑏)
249242, 248eqsstri 3502 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 × 𝑏) ↾ ) ⊆ ( × 𝑏)
250241, 249syl6ss 3484 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔) ⊆ ( × 𝑏))
25196, 250syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔) ⊆ ( × 𝑏))
25245resex 5254 . . . . . . . . . . . . . . . . . . . 20 (𝑔) ∈ V
253252elpw 4017 . . . . . . . . . . . . . . . . . . 19 ((𝑔) ∈ 𝒫 ( × 𝑏) ↔ (𝑔) ⊆ ( × 𝑏))
254251, 253sylibr 222 . . . . . . . . . . . . . . . . . 18 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔) ∈ 𝒫 ( × 𝑏))
255240, 254syl 17 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (𝑔) ∈ 𝒫 ( × 𝑏))
256 simpllr 794 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)))
257 psseq1 3560 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = → (𝑎𝑓𝑓))
258 xpeq1 4946 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = → (𝑎 × 𝑏) = ( × 𝑏))
259258pweqd 4016 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = → 𝒫 (𝑎 × 𝑏) = 𝒫 ( × 𝑏))
260 pweq 4014 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = → 𝒫 𝑎 = 𝒫 )
261260raleqdv 3025 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑)))
262 f1eq2 5893 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = → (𝑒:𝑎1-1→V ↔ 𝑒:1-1→V))
263262rexbidv 2938 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V))
264261, 263imbi12d 332 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V)))
265259, 264raleqbidv 3033 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 ( × 𝑏)(∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V)))
266257, 265imbi12d 332 . . . . . . . . . . . . . . . . . . 19 (𝑎 = → ((𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ (𝑓 → ∀𝑐 ∈ 𝒫 ( × 𝑏)(∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V))))
267266spv 2151 . . . . . . . . . . . . . . . . . 18 (∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) → (𝑓 → ∀𝑐 ∈ 𝒫 ( × 𝑏)(∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V)))
268256, 225, 267sylc 62 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑐 ∈ 𝒫 ( × 𝑏)(∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V))
269 imaeq1 5270 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = (𝑔) → (𝑐𝑑) = ((𝑔) “ 𝑑))
270269breq2d 4493 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑔) → (𝑑 ≼ (𝑐𝑑) ↔ 𝑑 ≼ ((𝑔) “ 𝑑)))
271270ralbidv 2873 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑔) → (∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑)))
272 pweq 4014 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑔) → 𝒫 𝑐 = 𝒫 (𝑔))
273272rexeqdv 3026 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑔) → (∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V))
274271, 273imbi12d 332 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝑔) → ((∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V)))
275274rspcva 3184 . . . . . . . . . . . . . . . . 17 (((𝑔) ∈ 𝒫 ( × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ( × 𝑏)(∀𝑑 ∈ 𝒫 𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:1-1→V)) → (∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V))
276255, 268, 275syl2anc 690 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (∀𝑑 ∈ 𝒫 𝑑 ≼ ((𝑔) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V))
277239, 276mpd 15 . . . . . . . . . . . . . . 15 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V)
278 f1eq1 5892 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑖 → (𝑒:1-1→V ↔ 𝑖:1-1→V))
279278cbvrexv 3052 . . . . . . . . . . . . . . 15 (∃𝑒 ∈ 𝒫 (𝑔)𝑒:1-1→V ↔ ∃𝑖 ∈ 𝒫 (𝑔)𝑖:1-1→V)
280277, 279sylib 206 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑖 ∈ 𝒫 (𝑔)𝑖:1-1→V)
281226ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔)) → 𝑓)
282281ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑓)
283 elpwi 4020 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ 𝒫 (𝑓) → 𝑐 ⊆ (𝑓))
284 difss 3603 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓) ⊆ 𝑓
285283, 284syl6ss 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ 𝒫 (𝑓) → 𝑐𝑓)
286285adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑐𝑓)
287282, 286unssd 3655 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) ⊆ 𝑓)
288130elpw2 4654 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐) ∈ 𝒫 𝑓 ↔ (𝑐) ⊆ 𝑓)
289287, 288sylibr 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) ∈ 𝒫 𝑓)
290 simprr 791 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))
291290ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))
292 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = (𝑐) → 𝑑 = (𝑐))
293 imaeq2 5271 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = (𝑐) → (𝑔𝑑) = (𝑔 “ (𝑐)))
294292, 293breq12d 4494 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑐) → (𝑑 ≼ (𝑔𝑑) ↔ (𝑐) ≼ (𝑔 “ (𝑐))))
295294rspcva 3184 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑐) ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → (𝑐) ≼ (𝑔 “ (𝑐)))
296289, 291, 295syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) ≼ (𝑔 “ (𝑐)))
297 imaundi 5354 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 “ (𝑐)) = ((𝑔) ∪ (𝑔𝑐))
298 undif2 3899 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔))) = ((𝑔) ∪ (𝑔𝑐))
299297, 298eqtr4i 2539 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 “ (𝑐)) = ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔)))
300296, 299syl6breq 4522 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) ≼ ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔))))
301 simp-4l 801 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑓 ∈ Fin)
302 ssfi 7939 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 ∈ Fin ∧ 𝑓) → ∈ Fin)
303301, 282, 302syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ∈ Fin)
304 vex 3080 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ∈ V
305304elpw 4017 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ 𝒫 𝑓𝑓)
306282, 305sylibr 222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ∈ 𝒫 𝑓)
307 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = 𝑑 = )
308 imaeq2 5271 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = → (𝑔𝑑) = (𝑔))
309307, 308breq12d 4494 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = → (𝑑 ≼ (𝑔𝑑) ↔ ≼ (𝑔)))
310309rspcva 3184 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑)) → ≼ (𝑔))
311306, 291, 310syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ≼ (𝑔))
312 simplrr 796 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ¬ ≺ (𝑔))
313 bren2 7746 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( ≈ (𝑔) ↔ ( ≼ (𝑔) ∧ ¬ ≺ (𝑔)))
314311, 312, 313sylanbrc 694 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ≈ (𝑔))
315314ensymd 7767 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑔) ≈ )
316 incom 3670 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐) = (𝑐)
317 ssdifin0 3905 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 ⊆ (𝑓) → (𝑐) = ∅)
318316, 317syl5eq 2560 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 ⊆ (𝑓) → (𝑐) = ∅)
319283, 318syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 ∈ 𝒫 (𝑓) → (𝑐) = ∅)
320319adantl 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (𝑐) = ∅)
321 disjdif 3895 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔) ∩ ((𝑔𝑐) ∖ (𝑔))) = ∅
322321a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ((𝑔) ∩ ((𝑔𝑐) ∖ (𝑔))) = ∅)
323 domunfican 7992 . . . . . . . . . . . . . . . . . . . . . . 23 ((( ∈ Fin ∧ (𝑔) ≈ ) ∧ ((𝑐) = ∅ ∧ ((𝑔) ∩ ((𝑔𝑐) ∖ (𝑔))) = ∅)) → ((𝑐) ≼ ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔))) ↔ 𝑐 ≼ ((𝑔𝑐) ∖ (𝑔))))
324303, 315, 320, 322, 323syl22anc 1318 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ((𝑐) ≼ ((𝑔) ∪ ((𝑔𝑐) ∖ (𝑔))) ↔ 𝑐 ≼ ((𝑔𝑐) ∖ (𝑔))))
325300, 324mpbid 220 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑐 ≼ ((𝑔𝑐) ∖ (𝑔)))
326103difeq1d 3593 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)) = ((𝑔𝑐) ∖ (𝑔)))
327326ad2antrl 759 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)) = ((𝑔𝑐) ∖ (𝑔)))
328327ad2antrr 757 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)) = ((𝑔𝑐) ∖ (𝑔)))
329325, 328breqtrrd 4509 . . . . . . . . . . . . . . . . . . . 20 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑐 ≼ (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)))
330 df-ss 3458 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 ⊆ (𝑓) ↔ (𝑐 ∩ (𝑓)) = 𝑐)
331283, 330sylib 206 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 ∈ 𝒫 (𝑓) → (𝑐 ∩ (𝑓)) = 𝑐)
332331imaeq2d 5275 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 ∈ 𝒫 (𝑓) → (𝑔 “ (𝑐 ∩ (𝑓))) = (𝑔𝑐))
333332ineq1d 3678 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ 𝒫 (𝑓) → ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) = ((𝑔𝑐) ∩ (𝑏 ∖ (𝑔))))
334 indif2 3732 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔𝑐) ∩ (𝑏 ∖ (𝑔))) = (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔))
335333, 334syl6eq 2564 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 ∈ 𝒫 (𝑓) → ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) = (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)))
336335adantl 480 . . . . . . . . . . . . . . . . . . . 20 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) = (((𝑔𝑐) ∩ 𝑏) ∖ (𝑔)))
337329, 336breqtrrd 4509 . . . . . . . . . . . . . . . . . . 19 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) ∧ 𝑐 ∈ 𝒫 (𝑓)) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))))
338337ralrimiva 2853 . . . . . . . . . . . . . . . . . 18 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑐 ∈ 𝒫 (𝑓)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))))
339 imainrect 5384 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔)))
340 imaeq2 5271 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑐) = ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
341339, 340syl5eqr 2562 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) = ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
342111, 341breq12d 4494 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑)))
343342cbvralv 3051 . . . . . . . . . . . . . . . . . 18 (∀𝑐 ∈ 𝒫 (𝑓)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓))) ∩ (𝑏 ∖ (𝑔))) ↔ ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
344338, 343sylib 206 . . . . . . . . . . . . . . . . 17 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
345344adantllr 750 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
346 inss2 3699 . . . . . . . . . . . . . . . . . . 19 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ⊆ ((𝑓) × (𝑏 ∖ (𝑔)))
347 difss 3603 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∖ (𝑔)) ⊆ 𝑏
348 xpss2 5045 . . . . . . . . . . . . . . . . . . . 20 ((𝑏 ∖ (𝑔)) ⊆ 𝑏 → ((𝑓) × (𝑏 ∖ (𝑔))) ⊆ ((𝑓) × 𝑏))
349347, 348ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑓) × (𝑏 ∖ (𝑔))) ⊆ ((𝑓) × 𝑏)
350346, 349sstri 3481 . . . . . . . . . . . . . . . . . 18 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ⊆ ((𝑓) × 𝑏)
35145inex1 4626 . . . . . . . . . . . . . . . . . . 19 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∈ V
352351elpw 4017 . . . . . . . . . . . . . . . . . 18 ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∈ 𝒫 ((𝑓) × 𝑏) ↔ (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ⊆ ((𝑓) × 𝑏))
353350, 352mpbir 219 . . . . . . . . . . . . . . . . 17 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∈ 𝒫 ((𝑓) × 𝑏)
354 incom 3670 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓) = (𝑓)
355 df-ss 3458 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 ↔ (𝑓) = )
356226, 355sylib 206 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 → (𝑓) = )
357354, 356syl5eq 2560 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 → (𝑓) = )
358357neeq1d 2745 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 → ((𝑓) ≠ ∅ ↔ ≠ ∅))
359358biimpar 500 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ≠ ∅) → (𝑓) ≠ ∅)
360 disj4 3880 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓) = ∅ ↔ ¬ (𝑓) ⊊ 𝑓)
361360bicomi 212 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑓) ⊊ 𝑓 ↔ (𝑓) = ∅)
362361necon1abii 2734 . . . . . . . . . . . . . . . . . . . 20 ((𝑓) ≠ ∅ ↔ (𝑓) ⊊ 𝑓)
363359, 362sylib 206 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ≠ ∅) → (𝑓) ⊊ 𝑓)
364363ad2antrl 759 . . . . . . . . . . . . . . . . . 18 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (𝑓) ⊊ 𝑓)
365 difexg 4634 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ V → (𝑓) ∈ V)
366130, 365ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑓) ∈ V
367 psseq1 3560 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑓) → (𝑎𝑓 ↔ (𝑓) ⊊ 𝑓))
368 xpeq1 4946 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑓) → (𝑎 × 𝑏) = ((𝑓) × 𝑏))
369368pweqd 4016 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑓) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓) × 𝑏))
370 pweq 4014 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑓) → 𝒫 𝑎 = 𝒫 (𝑓))
371370raleqdv 3025 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑓) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑)))
372 f1eq2 5893 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑓) → (𝑒:𝑎1-1→V ↔ 𝑒:(𝑓)–1-1→V))
373372rexbidv 2938 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑓) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V))
374371, 373imbi12d 332 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑓) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V)))
375369, 374raleqbidv 3033 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑓) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V)))
376367, 375imbi12d 332 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑓) → ((𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) ↔ ((𝑓) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V))))
377366, 376spcv 3176 . . . . . . . . . . . . . . . . . 18 (∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) → ((𝑓) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V)))
378256, 364, 377sylc 62 . . . . . . . . . . . . . . . . 17 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V))
379 imaeq1 5270 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → (𝑐𝑑) = ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑))
380379breq2d 4493 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → (𝑑 ≼ (𝑐𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑)))
381380ralbidv 2873 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑)))
382 pweq 4014 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))))
383382rexeqdv 3026 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V))
384381, 383imbi12d 332 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → ((∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V)))
385384rspcva 3184 . . . . . . . . . . . . . . . . 17 (((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∈ 𝒫 ((𝑓) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓)–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V))
386353, 378, 385sylancr 693 . . . . . . . . . . . . . . . 16 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (∀𝑑 ∈ 𝒫 (𝑓)𝑑 ≼ ((𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V))
387345, 386mpd 15 . . . . . . . . . . . . . . 15 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V)
388 f1eq1 5892 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑗 → (𝑒:(𝑓)–1-1→V ↔ 𝑗:(𝑓)–1-1→V))
389388cbvrexv 3052 . . . . . . . . . . . . . . 15 (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑒:(𝑓)–1-1→V ↔ ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V)
390387, 389sylib 206 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V)
391 elpwi 4020 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ 𝒫 (𝑔) → 𝑖 ⊆ (𝑔))
392 resss 5233 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔) ⊆ 𝑔
393391, 392syl6ss 3484 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ 𝒫 (𝑔) → 𝑖𝑔)
394393adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V) → 𝑖𝑔)
395394ad2antlr 758 . . . . . . . . . . . . . . . . . . . 20 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → 𝑖𝑔)
396 elpwi 4020 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → 𝑗 ⊆ (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))))
397 inss1 3698 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ⊆ 𝑔
398396, 397syl6ss 3484 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → 𝑗𝑔)
399398ad2antrl 759 . . . . . . . . . . . . . . . . . . . 20 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → 𝑗𝑔)
400395, 399unssd 3655 . . . . . . . . . . . . . . . . . . 19 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗) ⊆ 𝑔)
40145elpw2 4654 . . . . . . . . . . . . . . . . . . 19 ((𝑖𝑗) ∈ 𝒫 𝑔 ↔ (𝑖𝑗) ⊆ 𝑔)
402400, 401sylibr 222 . . . . . . . . . . . . . . . . . 18 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗) ∈ 𝒫 𝑔)
403 f1f1orn 5944 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖:1-1→V → 𝑖:1-1-onto→ran 𝑖)
404403adantl 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V) → 𝑖:1-1-onto→ran 𝑖)
405404ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → 𝑖:1-1-onto→ran 𝑖)
406 f1f1orn 5944 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗:(𝑓)–1-1→V → 𝑗:(𝑓)–1-1-onto→ran 𝑗)
407406ad2antll 760 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → 𝑗:(𝑓)–1-1-onto→ran 𝑗)
408 disjdif 3895 . . . . . . . . . . . . . . . . . . . . . . 23 ( ∩ (𝑓)) = ∅
409408a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ( ∩ (𝑓)) = ∅)
410 rnss 5166 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ⊆ (𝑔) → ran 𝑖 ⊆ ran (𝑔))
411391, 410syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ 𝒫 (𝑔) → ran 𝑖 ⊆ ran (𝑔))
412 df-ima 4945 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔) = ran (𝑔)
413411, 412syl6sseqr 3519 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ 𝒫 (𝑔) → ran 𝑖 ⊆ (𝑔))
414413adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V) → ran 𝑖 ⊆ (𝑔))
415414ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ran 𝑖 ⊆ (𝑔))
416 incom 3670 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔) ∩ ran 𝑗) = (ran 𝑗 ∩ (𝑔))
417396, 346syl6ss 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → 𝑗 ⊆ ((𝑓) × (𝑏 ∖ (𝑔))))
418 rnss 5166 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ⊆ ((𝑓) × (𝑏 ∖ (𝑔))) → ran 𝑗 ⊆ ran ((𝑓) × (𝑏 ∖ (𝑔))))
419417, 418syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → ran 𝑗 ⊆ ran ((𝑓) × (𝑏 ∖ (𝑔))))
420 rnxpss 5375 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ran ((𝑓) × (𝑏 ∖ (𝑔))) ⊆ (𝑏 ∖ (𝑔))
421419, 420syl6ss 3484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔)))
422421ad2antrl 759 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔)))
423 incom 3670 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑏 ∖ (𝑔)) ∩ (𝑔)) = ((𝑔) ∩ (𝑏 ∖ (𝑔)))
424 disjdif 3895 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔) ∩ (𝑏 ∖ (𝑔))) = ∅
425423, 424eqtri 2536 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 ∖ (𝑔)) ∩ (𝑔)) = ∅
426 ssdisj 3881 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ran 𝑗 ⊆ (𝑏 ∖ (𝑔)) ∧ ((𝑏 ∖ (𝑔)) ∩ (𝑔)) = ∅) → (ran 𝑗 ∩ (𝑔)) = ∅)
427422, 425, 426sylancl 692 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (ran 𝑗 ∩ (𝑔)) = ∅)
428416, 427syl5eq 2560 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ((𝑔) ∩ ran 𝑗) = ∅)
429 ssdisj 3881 . . . . . . . . . . . . . . . . . . . . . . 23 ((ran 𝑖 ⊆ (𝑔) ∧ ((𝑔) ∩ ran 𝑗) = ∅) → (ran 𝑖 ∩ ran 𝑗) = ∅)
430415, 428, 429syl2anc 690 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (ran 𝑖 ∩ ran 𝑗) = ∅)
431 f1oun 5952 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑖:1-1-onto→ran 𝑖𝑗:(𝑓)–1-1-onto→ran 𝑗) ∧ (( ∩ (𝑓)) = ∅ ∧ (ran 𝑖 ∩ ran 𝑗) = ∅)) → (𝑖𝑗):( ∪ (𝑓))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
432405, 407, 409, 430, 431syl22anc 1318 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗):( ∪ (𝑓))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
433 undif 3904 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 ↔ ( ∪ (𝑓)) = 𝑓)
434433biimpi 204 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 → ( ∪ (𝑓)) = 𝑓)
435434adantl 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) → ( ∪ (𝑓)) = 𝑓)
436435ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ( ∪ (𝑓)) = 𝑓)
437 f1oeq2 5924 . . . . . . . . . . . . . . . . . . . . . 22 (( ∪ (𝑓)) = 𝑓 → ((𝑖𝑗):( ∪ (𝑓))–1-1-onto→(ran 𝑖 ∪ ran 𝑗) ↔ (𝑖𝑗):𝑓1-1-onto→(ran 𝑖 ∪ ran 𝑗)))
438436, 437syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ((𝑖𝑗):( ∪ (𝑓))–1-1-onto→(ran 𝑖 ∪ ran 𝑗) ↔ (𝑖𝑗):𝑓1-1-onto→(ran 𝑖 ∪ ran 𝑗)))
439432, 438mpbid 220 . . . . . . . . . . . . . . . . . . . 20 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗):𝑓1-1-onto→(ran 𝑖 ∪ ran 𝑗))
440 f1of1 5932 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑗):𝑓1-1-onto→(ran 𝑖 ∪ ran 𝑗) → (𝑖𝑗):𝑓1-1→(ran 𝑖 ∪ ran 𝑗))
441439, 440syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗):𝑓1-1→(ran 𝑖 ∪ ran 𝑗))
442 ssv 3492 . . . . . . . . . . . . . . . . . . 19 (ran 𝑖 ∪ ran 𝑗) ⊆ V
443 f1ss 5902 . . . . . . . . . . . . . . . . . . 19 (((𝑖𝑗):𝑓1-1→(ran 𝑖 ∪ ran 𝑗) ∧ (ran 𝑖 ∪ ran 𝑗) ⊆ V) → (𝑖𝑗):𝑓1-1→V)
444441, 442, 443sylancl 692 . . . . . . . . . . . . . . . . . 18 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → (𝑖𝑗):𝑓1-1→V)
445 f1eq1 5892 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑖𝑗) → (𝑒:𝑓1-1→V ↔ (𝑖𝑗):𝑓1-1→V))
446445rspcev 3186 . . . . . . . . . . . . . . . . . 18 (((𝑖𝑗) ∈ 𝒫 𝑔 ∧ (𝑖𝑗):𝑓1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
447402, 444, 446syl2anc 690 . . . . . . . . . . . . . . . . 17 ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔)))) ∧ 𝑗:(𝑓)–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
448447rexlimdvaa 2918 . . . . . . . . . . . . . . . 16 (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔) ∧ 𝑖:1-1→V)) → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
449448rexlimdvaa 2918 . . . . . . . . . . . . . . 15 ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ 𝑓) → (∃𝑖 ∈ 𝒫 (𝑔)𝑖:1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
450240, 227, 449syl2anc 690 . . . . . . . . . . . . . 14 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → (∃𝑖 ∈ 𝒫 (𝑔)𝑖:1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓) × (𝑏 ∖ (𝑔))))𝑗:(𝑓)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
451280, 390, 450mp2d 46 . . . . . . . . . . . . 13 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
452451ex 448 . . . . . . . . . . . 12 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → (((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
453452exlimdv 1814 . . . . . . . . . . 11 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → (∃((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
454453imp 443 . . . . . . . . . 10 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ∃((𝑓 ≠ ∅) ∧ ¬ ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
455224, 454sylan2br 491 . . . . . . . . 9 (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) ∧ ¬ ∀((𝑓 ≠ ∅) → ≺ (𝑔))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
456223, 455pm2.61dan 827 . . . . . . . 8 ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)
457456exp32 628 . . . . . . 7 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V)))
458457ralrimiv 2852 . . . . . 6 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → ∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V))
459 imaeq1 5270 . . . . . . . . . 10 (𝑔 = 𝑐 → (𝑔𝑑) = (𝑐𝑑))
460459breq2d 4493 . . . . . . . . 9 (𝑔 = 𝑐 → (𝑑 ≼ (𝑔𝑑) ↔ 𝑑 ≼ (𝑐𝑑)))
461460ralbidv 2873 . . . . . . . 8 (𝑔 = 𝑐 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑)))
462 pweq 4014 . . . . . . . . 9 (𝑔 = 𝑐 → 𝒫 𝑔 = 𝒫 𝑐)
463462rexeqdv 3026 . . . . . . . 8 (𝑔 = 𝑐 → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))
464461, 463imbi12d 332 . . . . . . 7 (𝑔 = 𝑐 → ((∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V)))
465464cbvralv 3051 . . . . . 6 (∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))
466458, 465sylib 206 . . . . 5 (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))
467466exp31 627 . . . 4 (𝑓 ∈ Fin → (𝑏 ∈ Fin → (∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V)) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))))
468467a2d 29 . . 3 (𝑓 ∈ Fin → ((𝑏 ∈ Fin → ∀𝑎(𝑎𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))))
46922, 468syl5bi 230 . 2 (𝑓 ∈ Fin → (∀𝑎(𝑎𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓1-1→V))))
4709, 18, 469findcard3 7962 1 (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴1-1→V)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  wal 1472   = wceq 1474  wex 1694  wcel 1938  wne 2684  wral 2800  wrex 2801  Vcvv 3077  cdif 3441  cun 3442  cin 3443  wss 3444  wpss 3445  c0 3777  𝒫 cpw 4011  {csn 4028  cop 4034   class class class wbr 4481   × cxp 4930  ran crn 4933  cres 4934  cima 4935  1-1wf1 5686  1-1-ontowf1o 5688  cen 7712  cdom 7713  csdm 7714  Fincfn 7715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6721
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-om 6832  df-1o 7321  df-er 7503  df-en 7716  df-dom 7717  df-sdom 7718  df-fin 7719
This theorem is referenced by:  marypha1  8097
  Copyright terms: Public domain W3C validator