Metamath Proof Explorer

Theorem rabfodom

Description: Domination relation for restricted abstract class builders, based on a surjective function. (Contributed by Thierry Arnoux, 27-Jan-2020)

Ref Expression
Hypotheses rabfodom.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝜒 ↔ 𝜓 ) )
rabfodom.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
rabfodom.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 –onto→ 𝐵 )
Assertion rabfodom ( 𝜑 → { 𝑦 ∈ 𝐵 ∣ 𝜒 } ≼ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )

Proof

Step Hyp Ref Expression
1 rabfodom.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝜒 ↔ 𝜓 ) )
2 rabfodom.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 rabfodom.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 –onto→ 𝐵 )
4 vex ⊢ 𝑎 ∈ V
5 4 rabex ⊢ { 𝑥 ∈ 𝑎 ∣ 𝜓 } ∈ V
6 eqid ⊢ ( 𝑥 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑥 ) )
7 fof ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
8 3 7 syl ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
9 8 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
10 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
11 10 reseq1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) → ( 𝐹 ↾ 𝑎 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ 𝑎 ) )
12 elpwi ⊢ ( 𝑎 ∈ 𝒫 𝐴 → 𝑎 ⊆ 𝐴 )
13 12 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) → 𝑎 ⊆ 𝐴 )
14 13 resmptd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ 𝑎 ) = ( 𝑥 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑥 ) ) )
15 11 14 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) → ( 𝐹 ↾ 𝑎 ) = ( 𝑥 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑥 ) ) )
16 f1oeq1 ⊢ ( ( 𝐹 ↾ 𝑎 ) = ( 𝑥 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ↔ ( 𝑥 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑥 ) ) : 𝑎 –1-1-onto→ 𝐵 ) )
17 16 biimpa ⊢ ( ( ( 𝐹 ↾ 𝑎 ) = ( 𝑥 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) → ( 𝑥 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑥 ) ) : 𝑎 –1-1-onto→ 𝐵 )
18 15 17 sylancom ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) → ( 𝑥 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑥 ) ) : 𝑎 –1-1-onto→ 𝐵 )
19 simp1ll ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) ∧ 𝑥 ∈ 𝑎 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝜑 )
20 13 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) ∧ 𝑥 ∈ 𝑎 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝑎 ⊆ 𝐴 )
21 simp2 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) ∧ 𝑥 ∈ 𝑎 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝑥 ∈ 𝑎 )
22 20 21 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) ∧ 𝑥 ∈ 𝑎 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝑥 ∈ 𝐴 )
23 simp3 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) ∧ 𝑥 ∈ 𝑎 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝑦 = ( 𝐹 ‘ 𝑥 ) )
24 19 22 23 1 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) ∧ 𝑥 ∈ 𝑎 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝜒 ↔ 𝜓 ) )
25 6 18 24 f1oresrab ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) → ( ( 𝑥 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ { 𝑥 ∈ 𝑎 ∣ 𝜓 } ) : { 𝑥 ∈ 𝑎 ∣ 𝜓 } –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } )
26 f1oeng ⊢ ( ( { 𝑥 ∈ 𝑎 ∣ 𝜓 } ∈ V ∧ ( ( 𝑥 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ { 𝑥 ∈ 𝑎 ∣ 𝜓 } ) : { 𝑥 ∈ 𝑎 ∣ 𝜓 } –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ) → { 𝑥 ∈ 𝑎 ∣ 𝜓 } ≈ { 𝑦 ∈ 𝐵 ∣ 𝜒 } )
27 5 25 26 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) → { 𝑥 ∈ 𝑎 ∣ 𝜓 } ≈ { 𝑦 ∈ 𝐵 ∣ 𝜒 } )
28 27 ensymd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) → { 𝑦 ∈ 𝐵 ∣ 𝜒 } ≈ { 𝑥 ∈ 𝑎 ∣ 𝜓 } )
29 rabexg ⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ∈ V )
30 2 29 syl ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ∈ V )
31 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ∈ V )
32 rabss2 ⊢ ( 𝑎 ⊆ 𝐴 → { 𝑥 ∈ 𝑎 ∣ 𝜓 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )
33 13 32 syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) → { 𝑥 ∈ 𝑎 ∣ 𝜓 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )
34 ssdomg ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜓 } ∈ V → ( { 𝑥 ∈ 𝑎 ∣ 𝜓 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } → { 𝑥 ∈ 𝑎 ∣ 𝜓 } ≼ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) )
35 31 33 34 sylc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) → { 𝑥 ∈ 𝑎 ∣ 𝜓 } ≼ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )
36 endomtr ⊢ ( ( { 𝑦 ∈ 𝐵 ∣ 𝜒 } ≈ { 𝑥 ∈ 𝑎 ∣ 𝜓 } ∧ { 𝑥 ∈ 𝑎 ∣ 𝜓 } ≼ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) → { 𝑦 ∈ 𝐵 ∣ 𝜒 } ≼ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )
37 28 35 36 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 ) → { 𝑦 ∈ 𝐵 ∣ 𝜒 } ≼ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )
38 foresf1o ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ∃ 𝑎 ∈ 𝒫 𝐴 ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 )
39 2 3 38 syl2anc ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝒫 𝐴 ( 𝐹 ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝐵 )
40 37 39 r19.29a ⊢ ( 𝜑 → { 𝑦 ∈ 𝐵 ∣ 𝜒 } ≼ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )