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 snex ⊢ { 𝑖 } ∈ 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 df-ss ⊢ ( 𝑐 ⊆ ( 𝑓 ∖ { 𝑖 } ) ↔ ( 𝑐 ∩ ( 𝑓 ∖ { 𝑖 } ) ) = 𝑐 )
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 df-ss ⊢ ( ( 𝑔 “ 𝑐 ) ⊆ 𝑏 ↔ ( ( 𝑔 “ 𝑐 ) ∩ 𝑏 ) = ( 𝑔 “ 𝑐 ) )
101 99 100 sylib ⊢ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) → ( ( 𝑔 “ 𝑐 ) ∩ 𝑏 ) = ( 𝑔 “ 𝑐 ) )
102 101 difeq1d ⊢ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) → ( ( ( 𝑔 “ 𝑐 ) ∩ 𝑏 ) ∖ { 𝑗 } ) = ( ( 𝑔 “ 𝑐 ) ∖ { 𝑗 } ) )
103 102 ad2antrl ⊢ ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) → ( ( ( 𝑔 “ 𝑐 ) ∩ 𝑏 ) ∖ { 𝑗 } ) = ( ( 𝑔 “ 𝑐 ) ∖ { 𝑗 } ) )
104 92 103 syl5eq ⊢ ( ( ( 𝑓 ∈ 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 syl5eqr ⊢ ( 𝑐 = 𝑑 → ( ( 𝑔 “ ( 𝑐 ∩ ( 𝑓 ∖ { 𝑖 } ) ) ) ∩ ( 𝑏 ∖ { 𝑗 } ) ) = ( ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) “ 𝑑 ) )
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 incom ⊢ ( ( 𝑏 ∖ { 𝑗 } ) ∩ { 𝑗 } ) = ( { 𝑗 } ∩ ( 𝑏 ∖ { 𝑗 } ) )
180 disjdif ⊢ ( { 𝑗 } ∩ ( 𝑏 ∖ { 𝑗 } ) ) = ∅
181 179 180 eqtri ⊢ ( ( 𝑏 ∖ { 𝑗 } ) ∩ { 𝑗 } ) = ∅
182 ssdisj ⊢ ( ( ran 𝑘 ⊆ ( 𝑏 ∖ { 𝑗 } ) ∧ ( ( 𝑏 ∖ { 𝑗 } ) ∩ { 𝑗 } ) = ∅ ) → ( ran 𝑘 ∩ { 𝑗 } ) = ∅ )
183 178 181 182 sylancl ⊢ ( 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) → ( ran 𝑘 ∩ { 𝑗 } ) = ∅ )
184 173 183 syl5eq ⊢ ( 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) → ( { 𝑗 } ∩ ran 𝑘 ) = ∅ )
185 184 adantr ⊢ ( ( 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) ∧ 𝑘 : ( 𝑓 ∖ { 𝑖 } ) –1-1→ V ) → ( { 𝑗 } ∩ ran 𝑘 ) = ∅ )
186 f1oun ⊢ ( ( ( { ⟨ 𝑖 , 𝑗 ⟩ } : { 𝑖 } –1-1-onto→ { 𝑗 } ∧ 𝑘 : ( 𝑓 ∖ { 𝑖 } ) –1-1-onto→ ran 𝑘 ) ∧ ( ( { 𝑖 } ∩ ( 𝑓 ∖ { 𝑖 } ) ) = ∅ ∧ ( { 𝑗 } ∩ ran 𝑘 ) = ∅ ) ) → ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : ( { 𝑖 } ∪ ( 𝑓 ∖ { 𝑖 } ) ) –1-1-onto→ ( { 𝑗 } ∪ ran 𝑘 ) )
187 168 170 172 185 186 syl22anc ⊢ ( ( 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) ∧ 𝑘 : ( 𝑓 ∖ { 𝑖 } ) –1-1→ V ) → ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : ( { 𝑖 } ∪ ( 𝑓 ∖ { 𝑖 } ) ) –1-1-onto→ ( { 𝑗 } ∪ ran 𝑘 ) )
188 187 adantl ⊢ ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) ) ∧ ( 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) ∧ 𝑘 : ( 𝑓 ∖ { 𝑖 } ) –1-1→ V ) ) → ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : ( { 𝑖 } ∪ ( 𝑓 ∖ { 𝑖 } ) ) –1-1-onto→ ( { 𝑗 } ∪ ran 𝑘 ) )
189 snssi ⊢ ( 𝑖 ∈ 𝑓 → { 𝑖 } ⊆ 𝑓 )
190 189 ad2antrl ⊢ ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) ) → { 𝑖 } ⊆ 𝑓 )
191 undif ⊢ ( { 𝑖 } ⊆ 𝑓 ↔ ( { 𝑖 } ∪ ( 𝑓 ∖ { 𝑖 } ) ) = 𝑓 )
192 190 191 sylib ⊢ ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) ) → ( { 𝑖 } ∪ ( 𝑓 ∖ { 𝑖 } ) ) = 𝑓 )
193 192 f1oeq2d ⊢ ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) ) → ( ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : ( { 𝑖 } ∪ ( 𝑓 ∖ { 𝑖 } ) ) –1-1-onto→ ( { 𝑗 } ∪ ran 𝑘 ) ↔ ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : 𝑓 –1-1-onto→ ( { 𝑗 } ∪ ran 𝑘 ) ) )
194 193 adantr ⊢ ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) ) ∧ ( 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) ∧ 𝑘 : ( 𝑓 ∖ { 𝑖 } ) –1-1→ V ) ) → ( ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : ( { 𝑖 } ∪ ( 𝑓 ∖ { 𝑖 } ) ) –1-1-onto→ ( { 𝑗 } ∪ ran 𝑘 ) ↔ ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : 𝑓 –1-1-onto→ ( { 𝑗 } ∪ ran 𝑘 ) ) )
195 188 194 mpbid ⊢ ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) ) ∧ ( 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) ∧ 𝑘 : ( 𝑓 ∖ { 𝑖 } ) –1-1→ V ) ) → ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : 𝑓 –1-1-onto→ ( { 𝑗 } ∪ ran 𝑘 ) )
196 f1of1 ⊢ ( ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : 𝑓 –1-1-onto→ ( { 𝑗 } ∪ ran 𝑘 ) → ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : 𝑓 –1-1→ ( { 𝑗 } ∪ ran 𝑘 ) )
197 ssv ⊢ ( { 𝑗 } ∪ ran 𝑘 ) ⊆ V
198 f1ss ⊢ ( ( ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : 𝑓 –1-1→ ( { 𝑗 } ∪ ran 𝑘 ) ∧ ( { 𝑗 } ∪ ran 𝑘 ) ⊆ V ) → ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : 𝑓 –1-1→ V )
199 196 197 198 sylancl ⊢ ( ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : 𝑓 –1-1-onto→ ( { 𝑗 } ∪ ran 𝑘 ) → ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : 𝑓 –1-1→ V )
200 195 199 syl ⊢ ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) ) ∧ ( 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) ∧ 𝑘 : ( 𝑓 ∖ { 𝑖 } ) –1-1→ V ) ) → ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : 𝑓 –1-1→ V )
201 f1eq1 ⊢ ( 𝑒 = ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) → ( 𝑒 : 𝑓 –1-1→ V ↔ ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : 𝑓 –1-1→ V ) )
202 201 rspcev ⊢ ( ( ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) ∈ 𝒫 𝑔 ∧ ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ 𝑘 ) : 𝑓 –1-1→ V ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V )
203 166 200 202 syl2anc ⊢ ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) ) ∧ ( 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) ∧ 𝑘 : ( 𝑓 ∖ { 𝑖 } ) –1-1→ V ) ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V )
204 203 rexlimdvaa ⊢ ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) ) → ( ∃ 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) 𝑘 : ( 𝑓 ∖ { 𝑖 } ) –1-1→ V → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) )
205 204 ex ⊢ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) → ( ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) → ( ∃ 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) 𝑘 : ( 𝑓 ∖ { 𝑖 } ) –1-1→ V → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) ) )
206 205 adantr ⊢ ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) → ( ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) → ( ∃ 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) 𝑘 : ( 𝑓 ∖ { 𝑖 } ) –1-1→ V → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) ) )
207 206 ad2antlr ⊢ ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ( ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) → ( ∃ 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) 𝑘 : ( 𝑓 ∖ { 𝑖 } ) –1-1→ V → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) ) )
208 207 impr ⊢ ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) ∧ ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) ) ) → ( ∃ 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) 𝑘 : ( 𝑓 ∖ { 𝑖 } ) –1-1→ V → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) )
209 208 adantllr ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) ∧ ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) ) ) → ( ∃ 𝑘 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ { 𝑖 } ) × ( 𝑏 ∖ { 𝑗 } ) ) ) 𝑘 : ( 𝑓 ∖ { 𝑖 } ) –1-1→ V → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) )
210 153 209 mpd ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) ∧ ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) ) ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V )
211 210 expr ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ( ( 𝑖 ∈ 𝑓 ∧ 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) )
212 211 expd ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ( 𝑖 ∈ 𝑓 → ( 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) ) )
213 212 impr ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) ∧ 𝑖 ∈ 𝑓 ) ) → ( 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) )
214 213 exlimdv ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) ∧ 𝑖 ∈ 𝑓 ) ) → ( ∃ 𝑗 𝑗 ∈ ( 𝑔 “ { 𝑖 } ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) )
215 56 214 mpd ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) ∧ 𝑖 ∈ 𝑓 ) ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V )
216 215 expr ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ( 𝑖 ∈ 𝑓 → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) )
217 216 exlimdv ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ( ∃ 𝑖 𝑖 ∈ 𝑓 → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) )
218 32 217 syl5bi ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ( 𝑓 ≠ ∅ → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) )
219 31 218 pm2.61dne ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V )
220 exanali ⊢ ( ∃ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ↔ ¬ ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) )
221 simprll ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ℎ ⊊ 𝑓 )
222 pssss ⊢ ( ℎ ⊊ 𝑓 → ℎ ⊆ 𝑓 )
223 221 222 syl ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ℎ ⊆ 𝑓 )
224 sspwb ⊢ ( ℎ ⊆ 𝑓 ↔ 𝒫 ℎ ⊆ 𝒫 𝑓 )
225 223 224 sylib ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → 𝒫 ℎ ⊆ 𝒫 𝑓 )
226 simplrr ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) )
227 ssralv ⊢ ( 𝒫 ℎ ⊆ 𝒫 𝑓 → ( ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) → ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) )
228 225 226 227 sylc ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( 𝑔 “ 𝑑 ) )
229 elpwi ⊢ ( 𝑑 ∈ 𝒫 ℎ → 𝑑 ⊆ ℎ )
230 resima2 ⊢ ( 𝑑 ⊆ ℎ → ( ( 𝑔 ↾ ℎ ) “ 𝑑 ) = ( 𝑔 “ 𝑑 ) )
231 229 230 syl ⊢ ( 𝑑 ∈ 𝒫 ℎ → ( ( 𝑔 ↾ ℎ ) “ 𝑑 ) = ( 𝑔 “ 𝑑 ) )
232 231 eqcomd ⊢ ( 𝑑 ∈ 𝒫 ℎ → ( 𝑔 “ 𝑑 ) = ( ( 𝑔 ↾ ℎ ) “ 𝑑 ) )
233 232 breq2d ⊢ ( 𝑑 ∈ 𝒫 ℎ → ( 𝑑 ≼ ( 𝑔 “ 𝑑 ) ↔ 𝑑 ≼ ( ( 𝑔 ↾ ℎ ) “ 𝑑 ) ) )
234 233 ralbiia ⊢ ( ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( 𝑔 “ 𝑑 ) ↔ ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( ( 𝑔 ↾ ℎ ) “ 𝑑 ) )
235 228 234 sylib ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( ( 𝑔 ↾ ℎ ) “ 𝑑 ) )
236 imaeq1 ⊢ ( 𝑐 = ( 𝑔 ↾ ℎ ) → ( 𝑐 “ 𝑑 ) = ( ( 𝑔 ↾ ℎ ) “ 𝑑 ) )
237 236 breq2d ⊢ ( 𝑐 = ( 𝑔 ↾ ℎ ) → ( 𝑑 ≼ ( 𝑐 “ 𝑑 ) ↔ 𝑑 ≼ ( ( 𝑔 ↾ ℎ ) “ 𝑑 ) ) )
238 237 ralbidv ⊢ ( 𝑐 = ( 𝑔 ↾ ℎ ) → ( ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( 𝑐 “ 𝑑 ) ↔ ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( ( 𝑔 ↾ ℎ ) “ 𝑑 ) ) )
239 pweq ⊢ ( 𝑐 = ( 𝑔 ↾ ℎ ) → 𝒫 𝑐 = 𝒫 ( 𝑔 ↾ ℎ ) )
240 239 rexeqdv ⊢ ( 𝑐 = ( 𝑔 ↾ ℎ ) → ( ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ℎ –1-1→ V ↔ ∃ 𝑒 ∈ 𝒫 ( 𝑔 ↾ ℎ ) 𝑒 : ℎ –1-1→ V ) )
241 238 240 imbi12d ⊢ ( 𝑐 = ( 𝑔 ↾ ℎ ) → ( ( ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ℎ –1-1→ V ) ↔ ( ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( ( 𝑔 ↾ ℎ ) “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 ( 𝑔 ↾ ℎ ) 𝑒 : ℎ –1-1→ V ) ) )
242 simpllr ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) )
243 psseq1 ⊢ ( 𝑎 = ℎ → ( 𝑎 ⊊ 𝑓 ↔ ℎ ⊊ 𝑓 ) )
244 xpeq1 ⊢ ( 𝑎 = ℎ → ( 𝑎 × 𝑏 ) = ( ℎ × 𝑏 ) )
245 244 pweqd ⊢ ( 𝑎 = ℎ → 𝒫 ( 𝑎 × 𝑏 ) = 𝒫 ( ℎ × 𝑏 ) )
246 pweq ⊢ ( 𝑎 = ℎ → 𝒫 𝑎 = 𝒫 ℎ )
247 246 raleqdv ⊢ ( 𝑎 = ℎ → ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) ↔ ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( 𝑐 “ 𝑑 ) ) )
248 f1eq2 ⊢ ( 𝑎 = ℎ → ( 𝑒 : 𝑎 –1-1→ V ↔ 𝑒 : ℎ –1-1→ V ) )
249 248 rexbidv ⊢ ( 𝑎 = ℎ → ( ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ↔ ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ℎ –1-1→ V ) )
250 247 249 imbi12d ⊢ ( 𝑎 = ℎ → ( ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ↔ ( ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ℎ –1-1→ V ) ) )
251 245 250 raleqbidv ⊢ ( 𝑎 = ℎ → ( ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ↔ ∀ 𝑐 ∈ 𝒫 ( ℎ × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ℎ –1-1→ V ) ) )
252 243 251 imbi12d ⊢ ( 𝑎 = ℎ → ( ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ↔ ( ℎ ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( ℎ × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ℎ –1-1→ V ) ) ) )
253 252 spvv ⊢ ( ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) → ( ℎ ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( ℎ × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ℎ –1-1→ V ) ) )
254 242 221 253 sylc ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∀ 𝑐 ∈ 𝒫 ( ℎ × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ℎ –1-1→ V ) )
255 simplrl ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) )
256 ssres ⊢ ( 𝑔 ⊆ ( 𝑓 × 𝑏 ) → ( 𝑔 ↾ ℎ ) ⊆ ( ( 𝑓 × 𝑏 ) ↾ ℎ ) )
257 df-res ⊢ ( ( 𝑓 × 𝑏 ) ↾ ℎ ) = ( ( 𝑓 × 𝑏 ) ∩ ( ℎ × V ) )
258 inxp ⊢ ( ( 𝑓 × 𝑏 ) ∩ ( ℎ × V ) ) = ( ( 𝑓 ∩ ℎ ) × ( 𝑏 ∩ V ) )
259 inss2 ⊢ ( 𝑓 ∩ ℎ ) ⊆ ℎ
260 inss1 ⊢ ( 𝑏 ∩ V ) ⊆ 𝑏
261 xpss12 ⊢ ( ( ( 𝑓 ∩ ℎ ) ⊆ ℎ ∧ ( 𝑏 ∩ V ) ⊆ 𝑏 ) → ( ( 𝑓 ∩ ℎ ) × ( 𝑏 ∩ V ) ) ⊆ ( ℎ × 𝑏 ) )
262 259 260 261 mp2an ⊢ ( ( 𝑓 ∩ ℎ ) × ( 𝑏 ∩ V ) ) ⊆ ( ℎ × 𝑏 )
263 258 262 eqsstri ⊢ ( ( 𝑓 × 𝑏 ) ∩ ( ℎ × V ) ) ⊆ ( ℎ × 𝑏 )
264 257 263 eqsstri ⊢ ( ( 𝑓 × 𝑏 ) ↾ ℎ ) ⊆ ( ℎ × 𝑏 )
265 256 264 sstrdi ⊢ ( 𝑔 ⊆ ( 𝑓 × 𝑏 ) → ( 𝑔 ↾ ℎ ) ⊆ ( ℎ × 𝑏 ) )
266 94 265 syl ⊢ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) → ( 𝑔 ↾ ℎ ) ⊆ ( ℎ × 𝑏 ) )
267 45 resex ⊢ ( 𝑔 ↾ ℎ ) ∈ V
268 267 elpw ⊢ ( ( 𝑔 ↾ ℎ ) ∈ 𝒫 ( ℎ × 𝑏 ) ↔ ( 𝑔 ↾ ℎ ) ⊆ ( ℎ × 𝑏 ) )
269 266 268 sylibr ⊢ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) → ( 𝑔 ↾ ℎ ) ∈ 𝒫 ( ℎ × 𝑏 ) )
270 255 269 syl ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ( 𝑔 ↾ ℎ ) ∈ 𝒫 ( ℎ × 𝑏 ) )
271 241 254 270 rspcdva ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ( ∀ 𝑑 ∈ 𝒫 ℎ 𝑑 ≼ ( ( 𝑔 ↾ ℎ ) “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 ( 𝑔 ↾ ℎ ) 𝑒 : ℎ –1-1→ V ) )
272 235 271 mpd ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∃ 𝑒 ∈ 𝒫 ( 𝑔 ↾ ℎ ) 𝑒 : ℎ –1-1→ V )
273 f1eq1 ⊢ ( 𝑒 = 𝑖 → ( 𝑒 : ℎ –1-1→ V ↔ 𝑖 : ℎ –1-1→ V ) )
274 273 cbvrexvw ⊢ ( ∃ 𝑒 ∈ 𝒫 ( 𝑔 ↾ ℎ ) 𝑒 : ℎ –1-1→ V ↔ ∃ 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) 𝑖 : ℎ –1-1→ V )
275 272 274 sylib ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∃ 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) 𝑖 : ℎ –1-1→ V )
276 id ⊢ ( 𝑑 = ( ℎ ∪ 𝑐 ) → 𝑑 = ( ℎ ∪ 𝑐 ) )
277 imaeq2 ⊢ ( 𝑑 = ( ℎ ∪ 𝑐 ) → ( 𝑔 “ 𝑑 ) = ( 𝑔 “ ( ℎ ∪ 𝑐 ) ) )
278 276 277 breq12d ⊢ ( 𝑑 = ( ℎ ∪ 𝑐 ) → ( 𝑑 ≼ ( 𝑔 “ 𝑑 ) ↔ ( ℎ ∪ 𝑐 ) ≼ ( 𝑔 “ ( ℎ ∪ 𝑐 ) ) ) )
279 simprr ⊢ ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) → ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) )
280 279 ad2antrr ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) )
281 222 ad2antrr ⊢ ( ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) → ℎ ⊆ 𝑓 )
282 281 ad2antlr ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ℎ ⊆ 𝑓 )
283 elpwi ⊢ ( 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) → 𝑐 ⊆ ( 𝑓 ∖ ℎ ) )
284 difss ⊢ ( 𝑓 ∖ ℎ ) ⊆ 𝑓
285 283 284 sstrdi ⊢ ( 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) → 𝑐 ⊆ 𝑓 )
286 285 adantl ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → 𝑐 ⊆ 𝑓 )
287 282 286 unssd ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ( ℎ ∪ 𝑐 ) ⊆ 𝑓 )
288 128 elpw2 ⊢ ( ( ℎ ∪ 𝑐 ) ∈ 𝒫 𝑓 ↔ ( ℎ ∪ 𝑐 ) ⊆ 𝑓 )
289 287 288 sylibr ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ( ℎ ∪ 𝑐 ) ∈ 𝒫 𝑓 )
290 278 280 289 rspcdva ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ( ℎ ∪ 𝑐 ) ≼ ( 𝑔 “ ( ℎ ∪ 𝑐 ) ) )
291 imaundi ⊢ ( 𝑔 “ ( ℎ ∪ 𝑐 ) ) = ( ( 𝑔 “ ℎ ) ∪ ( 𝑔 “ 𝑐 ) )
292 undif2 ⊢ ( ( 𝑔 “ ℎ ) ∪ ( ( 𝑔 “ 𝑐 ) ∖ ( 𝑔 “ ℎ ) ) ) = ( ( 𝑔 “ ℎ ) ∪ ( 𝑔 “ 𝑐 ) )
293 291 292 eqtr4i ⊢ ( 𝑔 “ ( ℎ ∪ 𝑐 ) ) = ( ( 𝑔 “ ℎ ) ∪ ( ( 𝑔 “ 𝑐 ) ∖ ( 𝑔 “ ℎ ) ) )
294 290 293 breqtrdi ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ( ℎ ∪ 𝑐 ) ≼ ( ( 𝑔 “ ℎ ) ∪ ( ( 𝑔 “ 𝑐 ) ∖ ( 𝑔 “ ℎ ) ) ) )
295 simp-4l ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → 𝑓 ∈ Fin )
296 295 282 ssfid ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ℎ ∈ Fin )
297 id ⊢ ( 𝑑 = ℎ → 𝑑 = ℎ )
298 imaeq2 ⊢ ( 𝑑 = ℎ → ( 𝑔 “ 𝑑 ) = ( 𝑔 “ ℎ ) )
299 297 298 breq12d ⊢ ( 𝑑 = ℎ → ( 𝑑 ≼ ( 𝑔 “ 𝑑 ) ↔ ℎ ≼ ( 𝑔 “ ℎ ) ) )
300 vex ⊢ ℎ ∈ V
301 300 elpw ⊢ ( ℎ ∈ 𝒫 𝑓 ↔ ℎ ⊆ 𝑓 )
302 282 301 sylibr ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ℎ ∈ 𝒫 𝑓 )
303 299 280 302 rspcdva ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ℎ ≼ ( 𝑔 “ ℎ ) )
304 simplrr ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ¬ ℎ ≺ ( 𝑔 “ ℎ ) )
305 bren2 ⊢ ( ℎ ≈ ( 𝑔 “ ℎ ) ↔ ( ℎ ≼ ( 𝑔 “ ℎ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) )
306 303 304 305 sylanbrc ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ℎ ≈ ( 𝑔 “ ℎ ) )
307 306 ensymd ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ( 𝑔 “ ℎ ) ≈ ℎ )
308 incom ⊢ ( ℎ ∩ 𝑐 ) = ( 𝑐 ∩ ℎ )
309 ssdifin0 ⊢ ( 𝑐 ⊆ ( 𝑓 ∖ ℎ ) → ( 𝑐 ∩ ℎ ) = ∅ )
310 308 309 syl5eq ⊢ ( 𝑐 ⊆ ( 𝑓 ∖ ℎ ) → ( ℎ ∩ 𝑐 ) = ∅ )
311 283 310 syl ⊢ ( 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) → ( ℎ ∩ 𝑐 ) = ∅ )
312 311 adantl ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ( ℎ ∩ 𝑐 ) = ∅ )
313 disjdif ⊢ ( ( 𝑔 “ ℎ ) ∩ ( ( 𝑔 “ 𝑐 ) ∖ ( 𝑔 “ ℎ ) ) ) = ∅
314 313 a1i ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ( ( 𝑔 “ ℎ ) ∩ ( ( 𝑔 “ 𝑐 ) ∖ ( 𝑔 “ ℎ ) ) ) = ∅ )
315 domunfican ⊢ ( ( ( ℎ ∈ Fin ∧ ( 𝑔 “ ℎ ) ≈ ℎ ) ∧ ( ( ℎ ∩ 𝑐 ) = ∅ ∧ ( ( 𝑔 “ ℎ ) ∩ ( ( 𝑔 “ 𝑐 ) ∖ ( 𝑔 “ ℎ ) ) ) = ∅ ) ) → ( ( ℎ ∪ 𝑐 ) ≼ ( ( 𝑔 “ ℎ ) ∪ ( ( 𝑔 “ 𝑐 ) ∖ ( 𝑔 “ ℎ ) ) ) ↔ 𝑐 ≼ ( ( 𝑔 “ 𝑐 ) ∖ ( 𝑔 “ ℎ ) ) ) )
316 296 307 312 314 315 syl22anc ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ( ( ℎ ∪ 𝑐 ) ≼ ( ( 𝑔 “ ℎ ) ∪ ( ( 𝑔 “ 𝑐 ) ∖ ( 𝑔 “ ℎ ) ) ) ↔ 𝑐 ≼ ( ( 𝑔 “ 𝑐 ) ∖ ( 𝑔 “ ℎ ) ) ) )
317 294 316 mpbid ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → 𝑐 ≼ ( ( 𝑔 “ 𝑐 ) ∖ ( 𝑔 “ ℎ ) ) )
318 101 difeq1d ⊢ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) → ( ( ( 𝑔 “ 𝑐 ) ∩ 𝑏 ) ∖ ( 𝑔 “ ℎ ) ) = ( ( 𝑔 “ 𝑐 ) ∖ ( 𝑔 “ ℎ ) ) )
319 318 ad2antrl ⊢ ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) → ( ( ( 𝑔 “ 𝑐 ) ∩ 𝑏 ) ∖ ( 𝑔 “ ℎ ) ) = ( ( 𝑔 “ 𝑐 ) ∖ ( 𝑔 “ ℎ ) ) )
320 319 ad2antrr ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ( ( ( 𝑔 “ 𝑐 ) ∩ 𝑏 ) ∖ ( 𝑔 “ ℎ ) ) = ( ( 𝑔 “ 𝑐 ) ∖ ( 𝑔 “ ℎ ) ) )
321 317 320 breqtrrd ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → 𝑐 ≼ ( ( ( 𝑔 “ 𝑐 ) ∩ 𝑏 ) ∖ ( 𝑔 “ ℎ ) ) )
322 df-ss ⊢ ( 𝑐 ⊆ ( 𝑓 ∖ ℎ ) ↔ ( 𝑐 ∩ ( 𝑓 ∖ ℎ ) ) = 𝑐 )
323 283 322 sylib ⊢ ( 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) → ( 𝑐 ∩ ( 𝑓 ∖ ℎ ) ) = 𝑐 )
324 323 imaeq2d ⊢ ( 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) → ( 𝑔 “ ( 𝑐 ∩ ( 𝑓 ∖ ℎ ) ) ) = ( 𝑔 “ 𝑐 ) )
325 324 ineq1d ⊢ ( 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) → ( ( 𝑔 “ ( 𝑐 ∩ ( 𝑓 ∖ ℎ ) ) ) ∩ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) = ( ( 𝑔 “ 𝑐 ) ∩ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) )
326 indif2 ⊢ ( ( 𝑔 “ 𝑐 ) ∩ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) = ( ( ( 𝑔 “ 𝑐 ) ∩ 𝑏 ) ∖ ( 𝑔 “ ℎ ) )
327 325 326 syl6eq ⊢ ( 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) → ( ( 𝑔 “ ( 𝑐 ∩ ( 𝑓 ∖ ℎ ) ) ) ∩ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) = ( ( ( 𝑔 “ 𝑐 ) ∩ 𝑏 ) ∖ ( 𝑔 “ ℎ ) ) )
328 327 adantl ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → ( ( 𝑔 “ ( 𝑐 ∩ ( 𝑓 ∖ ℎ ) ) ) ∩ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) = ( ( ( 𝑔 “ 𝑐 ) ∩ 𝑏 ) ∖ ( 𝑔 “ ℎ ) ) )
329 321 328 breqtrrd ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) ) → 𝑐 ≼ ( ( 𝑔 “ ( 𝑐 ∩ ( 𝑓 ∖ ℎ ) ) ) ∩ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) )
330 329 ralrimiva ⊢ ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∀ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑐 ≼ ( ( 𝑔 “ ( 𝑐 ∩ ( 𝑓 ∖ ℎ ) ) ) ∩ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) )
331 imainrect ⊢ ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) “ 𝑐 ) = ( ( 𝑔 “ ( 𝑐 ∩ ( 𝑓 ∖ ℎ ) ) ) ∩ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) )
332 imaeq2 ⊢ ( 𝑐 = 𝑑 → ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) “ 𝑐 ) = ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) “ 𝑑 ) )
333 331 332 syl5eqr ⊢ ( 𝑐 = 𝑑 → ( ( 𝑔 “ ( 𝑐 ∩ ( 𝑓 ∖ ℎ ) ) ) ∩ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) = ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) “ 𝑑 ) )
334 109 333 breq12d ⊢ ( 𝑐 = 𝑑 → ( 𝑐 ≼ ( ( 𝑔 “ ( 𝑐 ∩ ( 𝑓 ∖ ℎ ) ) ) ∩ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ↔ 𝑑 ≼ ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) “ 𝑑 ) ) )
335 334 cbvralvw ⊢ ( ∀ 𝑐 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑐 ≼ ( ( 𝑔 “ ( 𝑐 ∩ ( 𝑓 ∖ ℎ ) ) ) ∩ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ↔ ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) “ 𝑑 ) )
336 330 335 sylib ⊢ ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) “ 𝑑 ) )
337 336 adantllr ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) “ 𝑑 ) )
338 inss2 ⊢ ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ⊆ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) )
339 difss ⊢ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ⊆ 𝑏
340 xpss2 ⊢ ( ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ⊆ 𝑏 → ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ⊆ ( ( 𝑓 ∖ ℎ ) × 𝑏 ) )
341 339 340 ax-mp ⊢ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ⊆ ( ( 𝑓 ∖ ℎ ) × 𝑏 )
342 338 341 sstri ⊢ ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ⊆ ( ( 𝑓 ∖ ℎ ) × 𝑏 )
343 45 inex1 ⊢ ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∈ V
344 343 elpw ⊢ ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∈ 𝒫 ( ( 𝑓 ∖ ℎ ) × 𝑏 ) ↔ ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ⊆ ( ( 𝑓 ∖ ℎ ) × 𝑏 ) )
345 342 344 mpbir ⊢ ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∈ 𝒫 ( ( 𝑓 ∖ ℎ ) × 𝑏 )
346 incom ⊢ ( 𝑓 ∩ ℎ ) = ( ℎ ∩ 𝑓 )
347 df-ss ⊢ ( ℎ ⊆ 𝑓 ↔ ( ℎ ∩ 𝑓 ) = ℎ )
348 222 347 sylib ⊢ ( ℎ ⊊ 𝑓 → ( ℎ ∩ 𝑓 ) = ℎ )
349 346 348 syl5eq ⊢ ( ℎ ⊊ 𝑓 → ( 𝑓 ∩ ℎ ) = ℎ )
350 349 neeq1d ⊢ ( ℎ ⊊ 𝑓 → ( ( 𝑓 ∩ ℎ ) ≠ ∅ ↔ ℎ ≠ ∅ ) )
351 350 biimpar ⊢ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ( 𝑓 ∩ ℎ ) ≠ ∅ )
352 disj4 ⊢ ( ( 𝑓 ∩ ℎ ) = ∅ ↔ ¬ ( 𝑓 ∖ ℎ ) ⊊ 𝑓 )
353 352 bicomi ⊢ ( ¬ ( 𝑓 ∖ ℎ ) ⊊ 𝑓 ↔ ( 𝑓 ∩ ℎ ) = ∅ )
354 353 necon1abii ⊢ ( ( 𝑓 ∩ ℎ ) ≠ ∅ ↔ ( 𝑓 ∖ ℎ ) ⊊ 𝑓 )
355 351 354 sylib ⊢ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ( 𝑓 ∖ ℎ ) ⊊ 𝑓 )
356 355 ad2antrl ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ( 𝑓 ∖ ℎ ) ⊊ 𝑓 )
357 128 difexi ⊢ ( 𝑓 ∖ ℎ ) ∈ V
358 psseq1 ⊢ ( 𝑎 = ( 𝑓 ∖ ℎ ) → ( 𝑎 ⊊ 𝑓 ↔ ( 𝑓 ∖ ℎ ) ⊊ 𝑓 ) )
359 xpeq1 ⊢ ( 𝑎 = ( 𝑓 ∖ ℎ ) → ( 𝑎 × 𝑏 ) = ( ( 𝑓 ∖ ℎ ) × 𝑏 ) )
360 359 pweqd ⊢ ( 𝑎 = ( 𝑓 ∖ ℎ ) → 𝒫 ( 𝑎 × 𝑏 ) = 𝒫 ( ( 𝑓 ∖ ℎ ) × 𝑏 ) )
361 pweq ⊢ ( 𝑎 = ( 𝑓 ∖ ℎ ) → 𝒫 𝑎 = 𝒫 ( 𝑓 ∖ ℎ ) )
362 361 raleqdv ⊢ ( 𝑎 = ( 𝑓 ∖ ℎ ) → ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) ↔ ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( 𝑐 “ 𝑑 ) ) )
363 f1eq2 ⊢ ( 𝑎 = ( 𝑓 ∖ ℎ ) → ( 𝑒 : 𝑎 –1-1→ V ↔ 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ) )
364 363 rexbidv ⊢ ( 𝑎 = ( 𝑓 ∖ ℎ ) → ( ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ↔ ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ) )
365 362 364 imbi12d ⊢ ( 𝑎 = ( 𝑓 ∖ ℎ ) → ( ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ↔ ( ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) )
366 360 365 raleqbidv ⊢ ( 𝑎 = ( 𝑓 ∖ ℎ ) → ( ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ↔ ∀ 𝑐 ∈ 𝒫 ( ( 𝑓 ∖ ℎ ) × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) )
367 358 366 imbi12d ⊢ ( 𝑎 = ( 𝑓 ∖ ℎ ) → ( ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ↔ ( ( 𝑓 ∖ ℎ ) ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( ( 𝑓 ∖ ℎ ) × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) ) )
368 357 367 spcv ⊢ ( ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) → ( ( 𝑓 ∖ ℎ ) ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( ( 𝑓 ∖ ℎ ) × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) )
369 242 356 368 sylc ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∀ 𝑐 ∈ 𝒫 ( ( 𝑓 ∖ ℎ ) × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ) )
370 imaeq1 ⊢ ( 𝑐 = ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) → ( 𝑐 “ 𝑑 ) = ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) “ 𝑑 ) )
371 370 breq2d ⊢ ( 𝑐 = ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) → ( 𝑑 ≼ ( 𝑐 “ 𝑑 ) ↔ 𝑑 ≼ ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) “ 𝑑 ) ) )
372 371 ralbidv ⊢ ( 𝑐 = ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) → ( ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( 𝑐 “ 𝑑 ) ↔ ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) “ 𝑑 ) ) )
373 pweq ⊢ ( 𝑐 = ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) → 𝒫 𝑐 = 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) )
374 373 rexeqdv ⊢ ( 𝑐 = ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) → ( ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ↔ ∃ 𝑒 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ) )
375 372 374 imbi12d ⊢ ( 𝑐 = ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) → ( ( ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ↔ ( ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) )
376 375 rspcva ⊢ ( ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∈ 𝒫 ( ( 𝑓 ∖ ℎ ) × 𝑏 ) ∧ ∀ 𝑐 ∈ 𝒫 ( ( 𝑓 ∖ ℎ ) × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ( ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ) )
377 345 369 376 sylancr ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ( ∀ 𝑑 ∈ 𝒫 ( 𝑓 ∖ ℎ ) 𝑑 ≼ ( ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ) )
378 337 377 mpd ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∃ 𝑒 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V )
379 f1eq1 ⊢ ( 𝑒 = 𝑗 → ( 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ↔ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) )
380 379 cbvrexvw ⊢ ( ∃ 𝑒 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) 𝑒 : ( 𝑓 ∖ ℎ ) –1-1→ V ↔ ∃ 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V )
381 378 380 sylib ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∃ 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V )
382 elpwi ⊢ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) → 𝑖 ⊆ ( 𝑔 ↾ ℎ ) )
383 resss ⊢ ( 𝑔 ↾ ℎ ) ⊆ 𝑔
384 382 383 sstrdi ⊢ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) → 𝑖 ⊆ 𝑔 )
385 384 adantr ⊢ ( ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) → 𝑖 ⊆ 𝑔 )
386 385 ad2antlr ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → 𝑖 ⊆ 𝑔 )
387 elpwi ⊢ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) → 𝑗 ⊆ ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) )
388 inss1 ⊢ ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ⊆ 𝑔
389 387 388 sstrdi ⊢ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) → 𝑗 ⊆ 𝑔 )
390 389 ad2antrl ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → 𝑗 ⊆ 𝑔 )
391 386 390 unssd ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ( 𝑖 ∪ 𝑗 ) ⊆ 𝑔 )
392 45 elpw2 ⊢ ( ( 𝑖 ∪ 𝑗 ) ∈ 𝒫 𝑔 ↔ ( 𝑖 ∪ 𝑗 ) ⊆ 𝑔 )
393 391 392 sylibr ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ( 𝑖 ∪ 𝑗 ) ∈ 𝒫 𝑔 )
394 f1f1orn ⊢ ( 𝑖 : ℎ –1-1→ V → 𝑖 : ℎ –1-1-onto→ ran 𝑖 )
395 394 adantl ⊢ ( ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) → 𝑖 : ℎ –1-1-onto→ ran 𝑖 )
396 395 ad2antlr ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → 𝑖 : ℎ –1-1-onto→ ran 𝑖 )
397 f1f1orn ⊢ ( 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V → 𝑗 : ( 𝑓 ∖ ℎ ) –1-1-onto→ ran 𝑗 )
398 397 ad2antll ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → 𝑗 : ( 𝑓 ∖ ℎ ) –1-1-onto→ ran 𝑗 )
399 disjdif ⊢ ( ℎ ∩ ( 𝑓 ∖ ℎ ) ) = ∅
400 399 a1i ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ( ℎ ∩ ( 𝑓 ∖ ℎ ) ) = ∅ )
401 rnss ⊢ ( 𝑖 ⊆ ( 𝑔 ↾ ℎ ) → ran 𝑖 ⊆ ran ( 𝑔 ↾ ℎ ) )
402 382 401 syl ⊢ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) → ran 𝑖 ⊆ ran ( 𝑔 ↾ ℎ ) )
403 df-ima ⊢ ( 𝑔 “ ℎ ) = ran ( 𝑔 ↾ ℎ )
404 402 403 sseqtrrdi ⊢ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) → ran 𝑖 ⊆ ( 𝑔 “ ℎ ) )
405 404 adantr ⊢ ( ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) → ran 𝑖 ⊆ ( 𝑔 “ ℎ ) )
406 405 ad2antlr ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ran 𝑖 ⊆ ( 𝑔 “ ℎ ) )
407 incom ⊢ ( ( 𝑔 “ ℎ ) ∩ ran 𝑗 ) = ( ran 𝑗 ∩ ( 𝑔 “ ℎ ) )
408 387 338 sstrdi ⊢ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) → 𝑗 ⊆ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) )
409 rnss ⊢ ( 𝑗 ⊆ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) → ran 𝑗 ⊆ ran ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) )
410 408 409 syl ⊢ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) → ran 𝑗 ⊆ ran ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) )
411 rnxpss ⊢ ran ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ⊆ ( 𝑏 ∖ ( 𝑔 “ ℎ ) )
412 410 411 sstrdi ⊢ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) → ran 𝑗 ⊆ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) )
413 412 ad2antrl ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ran 𝑗 ⊆ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) )
414 incom ⊢ ( ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ∩ ( 𝑔 “ ℎ ) ) = ( ( 𝑔 “ ℎ ) ∩ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) )
415 disjdif ⊢ ( ( 𝑔 “ ℎ ) ∩ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) = ∅
416 414 415 eqtri ⊢ ( ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ∩ ( 𝑔 “ ℎ ) ) = ∅
417 ssdisj ⊢ ( ( ran 𝑗 ⊆ ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ∧ ( ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ∩ ( 𝑔 “ ℎ ) ) = ∅ ) → ( ran 𝑗 ∩ ( 𝑔 “ ℎ ) ) = ∅ )
418 413 416 417 sylancl ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ( ran 𝑗 ∩ ( 𝑔 “ ℎ ) ) = ∅ )
419 407 418 syl5eq ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ( ( 𝑔 “ ℎ ) ∩ ran 𝑗 ) = ∅ )
420 ssdisj ⊢ ( ( ran 𝑖 ⊆ ( 𝑔 “ ℎ ) ∧ ( ( 𝑔 “ ℎ ) ∩ ran 𝑗 ) = ∅ ) → ( ran 𝑖 ∩ ran 𝑗 ) = ∅ )
421 406 419 420 syl2anc ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ( ran 𝑖 ∩ ran 𝑗 ) = ∅ )
422 f1oun ⊢ ( ( ( 𝑖 : ℎ –1-1-onto→ ran 𝑖 ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1-onto→ ran 𝑗 ) ∧ ( ( ℎ ∩ ( 𝑓 ∖ ℎ ) ) = ∅ ∧ ( ran 𝑖 ∩ ran 𝑗 ) = ∅ ) ) → ( 𝑖 ∪ 𝑗 ) : ( ℎ ∪ ( 𝑓 ∖ ℎ ) ) –1-1-onto→ ( ran 𝑖 ∪ ran 𝑗 ) )
423 396 398 400 421 422 syl22anc ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ( 𝑖 ∪ 𝑗 ) : ( ℎ ∪ ( 𝑓 ∖ ℎ ) ) –1-1-onto→ ( ran 𝑖 ∪ ran 𝑗 ) )
424 undif ⊢ ( ℎ ⊆ 𝑓 ↔ ( ℎ ∪ ( 𝑓 ∖ ℎ ) ) = 𝑓 )
425 424 biimpi ⊢ ( ℎ ⊆ 𝑓 → ( ℎ ∪ ( 𝑓 ∖ ℎ ) ) = 𝑓 )
426 425 adantl ⊢ ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) → ( ℎ ∪ ( 𝑓 ∖ ℎ ) ) = 𝑓 )
427 426 ad2antrr ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ( ℎ ∪ ( 𝑓 ∖ ℎ ) ) = 𝑓 )
428 427 f1oeq2d ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ( ( 𝑖 ∪ 𝑗 ) : ( ℎ ∪ ( 𝑓 ∖ ℎ ) ) –1-1-onto→ ( ran 𝑖 ∪ ran 𝑗 ) ↔ ( 𝑖 ∪ 𝑗 ) : 𝑓 –1-1-onto→ ( ran 𝑖 ∪ ran 𝑗 ) ) )
429 423 428 mpbid ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ( 𝑖 ∪ 𝑗 ) : 𝑓 –1-1-onto→ ( ran 𝑖 ∪ ran 𝑗 ) )
430 f1of1 ⊢ ( ( 𝑖 ∪ 𝑗 ) : 𝑓 –1-1-onto→ ( ran 𝑖 ∪ ran 𝑗 ) → ( 𝑖 ∪ 𝑗 ) : 𝑓 –1-1→ ( ran 𝑖 ∪ ran 𝑗 ) )
431 429 430 syl ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ( 𝑖 ∪ 𝑗 ) : 𝑓 –1-1→ ( ran 𝑖 ∪ ran 𝑗 ) )
432 ssv ⊢ ( ran 𝑖 ∪ ran 𝑗 ) ⊆ V
433 f1ss ⊢ ( ( ( 𝑖 ∪ 𝑗 ) : 𝑓 –1-1→ ( ran 𝑖 ∪ ran 𝑗 ) ∧ ( ran 𝑖 ∪ ran 𝑗 ) ⊆ V ) → ( 𝑖 ∪ 𝑗 ) : 𝑓 –1-1→ V )
434 431 432 433 sylancl ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ( 𝑖 ∪ 𝑗 ) : 𝑓 –1-1→ V )
435 f1eq1 ⊢ ( 𝑒 = ( 𝑖 ∪ 𝑗 ) → ( 𝑒 : 𝑓 –1-1→ V ↔ ( 𝑖 ∪ 𝑗 ) : 𝑓 –1-1→ V ) )
436 435 rspcev ⊢ ( ( ( 𝑖 ∪ 𝑗 ) ∈ 𝒫 𝑔 ∧ ( 𝑖 ∪ 𝑗 ) : 𝑓 –1-1→ V ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V )
437 393 434 436 syl2anc ⊢ ( ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) ∧ ( 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) ∧ 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V ) ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V )
438 437 rexlimdvaa ⊢ ( ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) ∧ ( 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) ∧ 𝑖 : ℎ –1-1→ V ) ) → ( ∃ 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) )
439 438 rexlimdvaa ⊢ ( ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ℎ ⊆ 𝑓 ) → ( ∃ 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) 𝑖 : ℎ –1-1→ V → ( ∃ 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) ) )
440 255 223 439 syl2anc ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ( ∃ 𝑖 ∈ 𝒫 ( 𝑔 ↾ ℎ ) 𝑖 : ℎ –1-1→ V → ( ∃ 𝑗 ∈ 𝒫 ( 𝑔 ∩ ( ( 𝑓 ∖ ℎ ) × ( 𝑏 ∖ ( 𝑔 “ ℎ ) ) ) ) 𝑗 : ( 𝑓 ∖ ℎ ) –1-1→ V → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) ) )
441 275 381 440 mp2d ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V )
442 441 ex ⊢ ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) → ( ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) )
443 442 exlimdv ⊢ ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) → ( ∃ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) )
444 443 imp ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ∃ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) ∧ ¬ ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V )
445 220 444 sylan2br ⊢ ( ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) ∧ ¬ ∀ ℎ ( ( ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅ ) → ℎ ≺ ( 𝑔 “ ℎ ) ) ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V )
446 219 445 pm2.61dan ⊢ ( ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) ∧ ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ∧ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ) ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V )
447 446 exp32 ⊢ ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) → ( 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) → ( ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) ) )
448 447 ralrimiv ⊢ ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) → ∀ 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) )
449 imaeq1 ⊢ ( 𝑔 = 𝑐 → ( 𝑔 “ 𝑑 ) = ( 𝑐 “ 𝑑 ) )
450 449 breq2d ⊢ ( 𝑔 = 𝑐 → ( 𝑑 ≼ ( 𝑔 “ 𝑑 ) ↔ 𝑑 ≼ ( 𝑐 “ 𝑑 ) ) )
451 450 ralbidv ⊢ ( 𝑔 = 𝑐 → ( ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) ↔ ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑐 “ 𝑑 ) ) )
452 pweq ⊢ ( 𝑔 = 𝑐 → 𝒫 𝑔 = 𝒫 𝑐 )
453 452 rexeqdv ⊢ ( 𝑔 = 𝑐 → ( ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ↔ ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑓 –1-1→ V ) )
454 451 453 imbi12d ⊢ ( 𝑔 = 𝑐 → ( ( ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) ↔ ( ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑓 –1-1→ V ) ) )
455 454 cbvralvw ⊢ ( ∀ 𝑔 ∈ 𝒫 ( 𝑓 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑔 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑔 𝑒 : 𝑓 –1-1→ V ) ↔ ∀ 𝑐 ∈ 𝒫 ( 𝑓 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑓 –1-1→ V ) )
456 448 455 sylib ⊢ ( ( ( 𝑓 ∈ Fin ∧ 𝑏 ∈ Fin ) ∧ ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) → ∀ 𝑐 ∈ 𝒫 ( 𝑓 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑓 –1-1→ V ) )
457 456 exp31 ⊢ ( 𝑓 ∈ Fin → ( 𝑏 ∈ Fin → ( ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) → ∀ 𝑐 ∈ 𝒫 ( 𝑓 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑓 –1-1→ V ) ) ) )
458 457 a2d ⊢ ( 𝑓 ∈ Fin → ( ( 𝑏 ∈ Fin → ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) → ( 𝑏 ∈ Fin → ∀ 𝑐 ∈ 𝒫 ( 𝑓 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑓 –1-1→ V ) ) ) )
459 22 458 syl5bi ⊢ ( 𝑓 ∈ Fin → ( ∀ 𝑎 ( 𝑎 ⊊ 𝑓 → ( 𝑏 ∈ Fin → ∀ 𝑐 ∈ 𝒫 ( 𝑎 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑎 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑎 –1-1→ V ) ) ) → ( 𝑏 ∈ Fin → ∀ 𝑐 ∈ 𝒫 ( 𝑓 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝑓 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝑓 –1-1→ V ) ) ) )
460 9 18 459 findcard3 ⊢ ( 𝐴 ∈ Fin → ( 𝑏 ∈ Fin → ∀ 𝑐 ∈ 𝒫 ( 𝐴 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑒 ∈ 𝒫 𝑐 𝑒 : 𝐴 –1-1→ V ) ) )