Theorem relpfrlem 45303

Description: Lemma for relpfr 45304. Proved without using the Axiom of Replacement. This is isofrlem 7296 with weaker hypotheses. (Contributed by Eric Schmidt, 11-Oct-2025.)

Hypotheses

Ref	Expression
relpfrlem.1	⊢ (𝜑 → 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵))
relpfrlem.2	⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)

Assertion

Ref	Expression
relpfrlem	⊢ (𝜑 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐻   𝜑,𝑥   𝑥,𝑅   𝑥,𝑆

Proof of Theorem relpfrlem

Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relpfrlem.1	. . . . . . 7 ⊢ (𝜑 → 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵))
2		relpf 45300	. . . . . . 7 ⊢ (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) → 𝐻:𝐴⟶𝐵)
3	1, 2	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)
4		ffn 6670	. . . . . . . 8 ⊢ (𝐻:𝐴⟶𝐵 → 𝐻 Fn 𝐴)
5		n0 4307	. . . . . . . . . 10 ⊢ (𝑥 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝑥)
6		fnfvima 7189	. . . . . . . . . . . . 13 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥) → (𝐻‘𝑦) ∈ (𝐻 “ 𝑥))
7	6	ne0d 4296	. . . . . . . . . . . 12 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥) → (𝐻 “ 𝑥) ≠ ∅)
8	7	3expia 1122	. . . . . . . . . . 11 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴) → (𝑦 ∈ 𝑥 → (𝐻 “ 𝑥) ≠ ∅))
9	8	exlimdv 1935	. . . . . . . . . 10 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 𝑦 ∈ 𝑥 → (𝐻 “ 𝑥) ≠ ∅))
10	5, 9	biimtrid 242	. . . . . . . . 9 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴) → (𝑥 ≠ ∅ → (𝐻 “ 𝑥) ≠ ∅))
11	10	expimpd 453	. . . . . . . 8 ⊢ (𝐻 Fn 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝐻 “ 𝑥) ≠ ∅))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝐻:𝐴⟶𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝐻 “ 𝑥) ≠ ∅))
13		fimass 6690	. . . . . . 7 ⊢ (𝐻:𝐴⟶𝐵 → (𝐻 “ 𝑥) ⊆ 𝐵)
14	12, 13	jctild 525	. . . . . 6 ⊢ (𝐻:𝐴⟶𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅)))
15	3, 14	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅)))
16		dffr3 6066	. . . . . 6 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑧((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅))
17		relpfrlem.2	. . . . . . 7 ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)
18		sseq1 3961	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 “ 𝑥) → (𝑧 ⊆ 𝐵 ↔ (𝐻 “ 𝑥) ⊆ 𝐵))
19		neeq1 2995	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 “ 𝑥) → (𝑧 ≠ ∅ ↔ (𝐻 “ 𝑥) ≠ ∅))
20	18, 19	anbi12d 633	. . . . . . . . 9 ⊢ (𝑧 = (𝐻 “ 𝑥) → ((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) ↔ ((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅)))
21		ineq1 4167	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐻 “ 𝑥) → (𝑧 ∩ (◡𝑆 “ {𝑤})) = ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})))
22	21	eqeq1d 2739	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 “ 𝑥) → ((𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅ ↔ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅))
23	22	rexeqbi1dv 3311	. . . . . . . . 9 ⊢ (𝑧 = (𝐻 “ 𝑥) → (∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅ ↔ ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅))
24	20, 23	imbi12d 344	. . . . . . . 8 ⊢ (𝑧 = (𝐻 “ 𝑥) → (((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅) ↔ (((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
25	24	spcgv 3552	. . . . . . 7 ⊢ ((𝐻 “ 𝑥) ∈ V → (∀𝑧((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅) → (((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
26	17, 25	syl 17	. . . . . 6 ⊢ (𝜑 → (∀𝑧((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅) → (((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
27	16, 26	biimtrid 242	. . . . 5 ⊢ (𝜑 → (𝑆 Fr 𝐵 → (((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
28	15, 27	syl5d 73	. . . 4 ⊢ (𝜑 → (𝑆 Fr 𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
29	3	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → 𝐻:𝐴⟶𝐵)
30	29	ffund 6674	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → Fun 𝐻)
31		simpl 482	. . . . . . . . . 10 ⊢ ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → 𝑤 ∈ (𝐻 “ 𝑥))
32		fvelima 6907	. . . . . . . . . 10 ⊢ ((Fun 𝐻 ∧ 𝑤 ∈ (𝐻 “ 𝑥)) → ∃𝑦 ∈ 𝑥 (𝐻‘𝑦) = 𝑤)
33	30, 31, 32	syl2an 597	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → ∃𝑦 ∈ 𝑥 (𝐻‘𝑦) = 𝑤)
34		sneq 4592	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = (𝐻‘𝑦) → {𝑤} = {(𝐻‘𝑦)})
35	34	eqcoms 2745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐻‘𝑦) = 𝑤 → {𝑤} = {(𝐻‘𝑦)})
36	35	imaeq2d 6027	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐻‘𝑦) = 𝑤 → (◡𝑆 “ {𝑤}) = (◡𝑆 “ {(𝐻‘𝑦)}))
37	36	ineq2d 4174	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐻‘𝑦) = 𝑤 → ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})))
38	37	eqeq1d 2739	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻‘𝑦) = 𝑤 → (((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ ↔ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ∅))
39	38	biimpd 229	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐻‘𝑦) = 𝑤 → (((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ → ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ∅))
40		ssel 3929	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ⊆ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴))
41	40	imdistani 568	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥) → (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐴))
42		relpmin 45302	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ∅ → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
43	1, 41, 42	syl2an 597	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥)) → (((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ∅ → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
44	39, 43	sylan9r 508	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥)) ∧ (𝐻‘𝑦) = 𝑤) → (((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
45	44	adantld 490	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥)) ∧ (𝐻‘𝑦) = 𝑤) → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
46	45	exp42 435	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ⊆ 𝐴 → (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))))
47	46	imp 406	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))))
48	47	com3l 89	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → ((𝜑 ∧ 𝑥 ⊆ 𝐴) → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))))
49	48	com4t 93	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))))
50	49	imp 406	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
51	50	reximdvai 3149	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → (∃𝑦 ∈ 𝑥 (𝐻‘𝑦) = 𝑤 → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
52	33, 51	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)
53	52	rexlimdvaa 3140	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
54	53	ex 412	. . . . . 6 ⊢ (𝜑 → (𝑥 ⊆ 𝐴 → (∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
55	54	adantrd 491	. . . . 5 ⊢ (𝜑 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
56	55	a2d 29	. . . 4 ⊢ (𝜑 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
57	28, 56	syld 47	. . 3 ⊢ (𝜑 → (𝑆 Fr 𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
58	57	alrimdv 1931	. 2 ⊢ (𝜑 → (𝑆 Fr 𝐵 → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
59		dffr3 6066	. 2 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
60	58, 59	imbitrrdi 252	1 ⊢ (𝜑 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  ∃wrex 3062  Vcvv 3442   ∩ cin 3902   ⊆ wss 3903  ∅c0 4287  {csn 4582   Fr wfr 5582  ^◡ccnv 5631   “ cima 5635  Fun wfun 6494   Fn wfn 6495  ⟶wf 6496  ‘cfv 6500   RelPres wrelp 45292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-fr 5585  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-relp 45293

This theorem is referenced by:  relpfr  45304