Metamath Proof Explorer

Theorem marypha1lem

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

Ref Expression
Assertion marypha1lem ( 𝐴 ∈ Fin → ( 𝑏 ∈ Fin → ∀ 𝑐 ∈ 𝒫 ( 𝐴 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝐴 –1-1→ V ) ) )

Proof

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