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	$⊢ (φ \land x \in A \land y = F (x)) \to (χ \leftrightarrow ψ)$
	rabfodom.2	$⊢ φ \to A \in V$
	rabfodom.3	$⊢ φ \to F : A \underset{onto}{⟶} B$
Assertion	rabfodom	$⊢ φ \to \{y \in B \| χ\} ≼ \{x \in A \| ψ\}$

Proof

Step	Hyp	Ref	Expression
1		rabfodom.1	$⊢ (φ \land x \in A \land y = F (x)) \to (χ \leftrightarrow ψ)$
2		rabfodom.2	$⊢ φ \to A \in V$
3		rabfodom.3	$⊢ φ \to F : A \underset{onto}{⟶} B$
4		vex	$⊢ a \in V$
5	4	rabex	$⊢ \{x \in a \| ψ\} \in V$
6		eqid	$⊢ (x \in a ⟼ F (x)) = (x \in a ⟼ F (x))$
7		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
8	3 7	syl	$⊢ φ \to F : A ⟶ B$
9	8	feqmptd	$⊢ φ \to F = (x \in A ⟼ F (x))$
10	9	ad2antrr	$⊢ ((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \to F = (x \in A ⟼ F (x))$
11	10	reseq1d	$⊢ ((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \to {F ↾}_{a} = {(x \in A ⟼ F (x)) ↾}_{a}$
12		elpwi	$⊢ a \in 𝒫 A \to a \subseteq A$
13	12	ad2antlr	$⊢ ((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \to a \subseteq A$
14	13	resmptd	$⊢ ((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \to {(x \in A ⟼ F (x)) ↾}_{a} = (x \in a ⟼ F (x))$
15	11 14	eqtrd	$⊢ ((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \to {F ↾}_{a} = (x \in a ⟼ F (x))$
16		f1oeq1	$⊢ {F ↾}_{a} = (x \in a ⟼ F (x)) \to (({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B \leftrightarrow (x \in a ⟼ F (x)) : a \underset{1-1 onto}{⟶} B)$
17	16	biimpa	$⊢ ({F ↾}_{a} = (x \in a ⟼ F (x)) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \to (x \in a ⟼ F (x)) : a \underset{1-1 onto}{⟶} B$
18	15 17	sylancom	$⊢ ((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \to (x \in a ⟼ F (x)) : a \underset{1-1 onto}{⟶} B$
19		simp1ll	$⊢ (((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \land x \in a \land y = F (x)) \to φ$
20	13	3ad2ant1	$⊢ (((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \land x \in a \land y = F (x)) \to a \subseteq A$
21		simp2	$⊢ (((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \land x \in a \land y = F (x)) \to x \in a$
22	20 21	sseldd	$⊢ (((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \land x \in a \land y = F (x)) \to x \in A$
23		simp3	$⊢ (((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \land x \in a \land y = F (x)) \to y = F (x)$
24	19 22 23 1	syl3anc	$⊢ (((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \land x \in a \land y = F (x)) \to (χ \leftrightarrow ψ)$
25	6 18 24	f1oresrab	$⊢ ((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \to ({(x \in a ⟼ F (x)) ↾}_{\{x \in a \| ψ\}}) : \{x \in a \| ψ\} \underset{1-1 onto}{⟶} \{y \in B \| χ\}$
26		f1oeng	$⊢ (\{x \in a \| ψ\} \in V \land ({(x \in a ⟼ F (x)) ↾}_{\{x \in a \| ψ\}}) : \{x \in a \| ψ\} \underset{1-1 onto}{⟶} \{y \in B \| χ\}) \to \{x \in a \| ψ\} \approx \{y \in B \| χ\}$
27	5 25 26	sylancr	$⊢ ((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \to \{x \in a \| ψ\} \approx \{y \in B \| χ\}$
28	27	ensymd	$⊢ ((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \to \{y \in B \| χ\} \approx \{x \in a \| ψ\}$
29		rabexg	$⊢ A \in V \to \{x \in A \| ψ\} \in V$
30	2 29	syl	$⊢ φ \to \{x \in A \| ψ\} \in V$
31	30	ad2antrr	$⊢ ((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \to \{x \in A \| ψ\} \in V$
32		rabss2	$⊢ a \subseteq A \to \{x \in a \| ψ\} \subseteq \{x \in A \| ψ\}$
33	13 32	syl	$⊢ ((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \to \{x \in a \| ψ\} \subseteq \{x \in A \| ψ\}$
34		ssdomg	$⊢ \{x \in A \| ψ\} \in V \to (\{x \in a \| ψ\} \subseteq \{x \in A \| ψ\} \to \{x \in a \| ψ\} ≼ \{x \in A \| ψ\})$
35	31 33 34	sylc	$⊢ ((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \to \{x \in a \| ψ\} ≼ \{x \in A \| ψ\}$
36		endomtr	$⊢ (\{y \in B \| χ\} \approx \{x \in a \| ψ\} \land \{x \in a \| ψ\} ≼ \{x \in A \| ψ\}) \to \{y \in B \| χ\} ≼ \{x \in A \| ψ\}$
37	28 35 36	syl2anc	$⊢ ((φ \land a \in 𝒫 A) \land ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B) \to \{y \in B \| χ\} ≼ \{x \in A \| ψ\}$
38		foresf1o	$⊢ (A \in V \land F : A \underset{onto}{⟶} B) \to \exists a \in 𝒫 A ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B$
39	2 3 38	syl2anc	$⊢ φ \to \exists a \in 𝒫 A ({F ↾}_{a}) : a \underset{1-1 onto}{⟶} B$
40	37 39	r19.29a	$⊢ φ \to \{y \in B \| χ\} ≼ \{x \in A \| ψ\}$

Metamath Proof Explorer

Theorem rabfodom

Proof