Theorem relpfrlem 45070

Description: Lemma for relpfr 45071. Proved without using the Axiom of Replacement. This is isofrlem 7280 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 45067	. . . . . . 7 ⊢ (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) → 𝐻:𝐴⟶𝐵)
3	1, 2	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)
4		ffn 6656	. . . . . . . 8 ⊢ (𝐻:𝐴⟶𝐵 → 𝐻 Fn 𝐴)
5		n0 4302	. . . . . . . . . 10 ⊢ (𝑥 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝑥)
6		fnfvima 7173	. . . . . . . . . . . . 13 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥) → (𝐻‘𝑦) ∈ (𝐻 “ 𝑥))
7	6	ne0d 4291	. . . . . . . . . . . 12 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥) → (𝐻 “ 𝑥) ≠ ∅)
8	7	3expia 1121	. . . . . . . . . . 11 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴) → (𝑦 ∈ 𝑥 → (𝐻 “ 𝑥) ≠ ∅))
9	8	exlimdv 1934	. . . . . . . . . 10 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 𝑦 ∈ 𝑥 → (𝐻 “ 𝑥) ≠ ∅))
10	5, 9	biimtrid 242	. . . . . . . . 9 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴) → (𝑥 ≠ ∅ → (𝐻 “ 𝑥) ≠ ∅))
11	10	expimpd 453	. . . . . . . 8 ⊢ (𝐻 Fn 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝐻 “ 𝑥) ≠ ∅))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝐻:𝐴⟶𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝐻 “ 𝑥) ≠ ∅))
13		fimass 6676	. . . . . . 7 ⊢ (𝐻:𝐴⟶𝐵 → (𝐻 “ 𝑥) ⊆ 𝐵)
14	12, 13	jctild 525	. . . . . 6 ⊢ (𝐻:𝐴⟶𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅)))
15	3, 14	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅)))
16		dffr3 6052	. . . . . 6 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑧((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅))
17		relpfrlem.2	. . . . . . 7 ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)
18		sseq1 3956	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 “ 𝑥) → (𝑧 ⊆ 𝐵 ↔ (𝐻 “ 𝑥) ⊆ 𝐵))
19		neeq1 2991	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 “ 𝑥) → (𝑧 ≠ ∅ ↔ (𝐻 “ 𝑥) ≠ ∅))
20	18, 19	anbi12d 632	. . . . . . . . 9 ⊢ (𝑧 = (𝐻 “ 𝑥) → ((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) ↔ ((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅)))
21		ineq1 4162	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐻 “ 𝑥) → (𝑧 ∩ (◡𝑆 “ {𝑤})) = ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})))
22	21	eqeq1d 2735	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 “ 𝑥) → ((𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅ ↔ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅))
23	22	rexeqbi1dv 3306	. . . . . . . . 9 ⊢ (𝑧 = (𝐻 “ 𝑥) → (∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅ ↔ ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅))
24	20, 23	imbi12d 344	. . . . . . . 8 ⊢ (𝑧 = (𝐻 “ 𝑥) → (((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅) ↔ (((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
25	24	spcgv 3547	. . . . . . 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 6660	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → Fun 𝐻)
31		simpl 482	. . . . . . . . . 10 ⊢ ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → 𝑤 ∈ (𝐻 “ 𝑥))
32		fvelima 6893	. . . . . . . . . 10 ⊢ ((Fun 𝐻 ∧ 𝑤 ∈ (𝐻 “ 𝑥)) → ∃𝑦 ∈ 𝑥 (𝐻‘𝑦) = 𝑤)
33	30, 31, 32	syl2an 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → ∃𝑦 ∈ 𝑥 (𝐻‘𝑦) = 𝑤)
34		sneq 4585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = (𝐻‘𝑦) → {𝑤} = {(𝐻‘𝑦)})
35	34	eqcoms 2741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐻‘𝑦) = 𝑤 → {𝑤} = {(𝐻‘𝑦)})
36	35	imaeq2d 6013	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐻‘𝑦) = 𝑤 → (◡𝑆 “ {𝑤}) = (◡𝑆 “ {(𝐻‘𝑦)}))
37	36	ineq2d 4169	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐻‘𝑦) = 𝑤 → ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})))
38	37	eqeq1d 2735	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻‘𝑦) = 𝑤 → (((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ ↔ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ∅))
39	38	biimpd 229	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐻‘𝑦) = 𝑤 → (((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ → ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ∅))
40		ssel 3924	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ⊆ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴))
41	40	imdistani 568	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥) → (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐴))
42		relpmin 45069	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ∅ → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
43	1, 41, 42	syl2an 596	. . . . . . . . . . . . . . . . 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 3144	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → (∃𝑦 ∈ 𝑥 (𝐻‘𝑦) = 𝑤 → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
52	33, 51	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)
53	52	rexlimdvaa 3135	. . . . . . 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 1930	. 2 ⊢ (𝜑 → (𝑆 Fr 𝐵 → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
59		dffr3 6052	. 2 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
60	58, 59	imbitrrdi 252	1 ⊢ (𝜑 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2929  ∃wrex 3057  Vcvv 3437   ∩ cin 3897   ⊆ wss 3898  ∅c0 4282  {csn 4575   Fr wfr 5569  ^◡ccnv 5618   “ cima 5622  Fun wfun 6480   Fn wfn 6481  ⟶wf 6482  ‘cfv 6486   RelPres wrelp 45059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-id 5514  df-fr 5572  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-relp 45060

This theorem is referenced by:  relpfr  45071