Theorem relpfrlem 45895

Description: Lemma for relpfr 45896. Proved without using the Axiom of Replacement. This is isofrlem 7340 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 45892	. . . . . . 7 ⊢ (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) → 𝐻:𝐴⟶𝐵)
3	1, 2	syl 18	. . . . . 6 ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)
4		ffn 6701	. . . . . . . 8 ⊢ (𝐻:𝐴⟶𝐵 → 𝐻 Fn 𝐴)
5		n0 4300	. . . . . . . . . 10 ⊢ (𝑥 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝑥)
6		fnfvima 7231	. . . . . . . . . . . . 13 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥) → (𝐻‘𝑦) ∈ (𝐻 “ 𝑥))
7	6	ne0d 4288	. . . . . . . . . . . 12 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥) → (𝐻 “ 𝑥) ≠ ∅)
8	7	3expia 1139	. . . . . . . . . . 11 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴) → (𝑦 ∈ 𝑥 → (𝐻 “ 𝑥) ≠ ∅))
9	8	exlimdv 1966	. . . . . . . . . 10 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 𝑦 ∈ 𝑥 → (𝐻 “ 𝑥) ≠ ∅))
10	5, 9	biimtrid 245	. . . . . . . . 9 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴) → (𝑥 ≠ ∅ → (𝐻 “ 𝑥) ≠ ∅))
11	10	expimpd 459	. . . . . . . 8 ⊢ (𝐻 Fn 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝐻 “ 𝑥) ≠ ∅))
12	4, 11	syl 18	. . . . . . 7 ⊢ (𝐻:𝐴⟶𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝐻 “ 𝑥) ≠ ∅))
13		fimass 6722	. . . . . . 7 ⊢ (𝐻:𝐴⟶𝐵 → (𝐻 “ 𝑥) ⊆ 𝐵)
14	12, 13	jctild 535	. . . . . 6 ⊢ (𝐻:𝐴⟶𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅)))
15	3, 14	syl 18	. . . . 5 ⊢ (𝜑 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅)))
16		dffr3 6093	. . . . . 6 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑧((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅))
17		relpfrlem.2	. . . . . . 7 ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)
18		sseq1 3956	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 “ 𝑥) → (𝑧 ⊆ 𝐵 ↔ (𝐻 “ 𝑥) ⊆ 𝐵))
19		neeq1 3018	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 “ 𝑥) → (𝑧 ≠ ∅ ↔ (𝐻 “ 𝑥) ≠ ∅))
20	18, 19	anbi12d 644	. . . . . . . . 9 ⊢ (𝑧 = (𝐻 “ 𝑥) → ((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) ↔ ((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅)))
21		ineq1 4159	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐻 “ 𝑥) → (𝑧 ∩ (◡𝑆 “ {𝑤})) = ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})))
22	21	eqeq1d 2763	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 “ 𝑥) → ((𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅ ↔ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅))
23	22	rexeqbi1dv 3331	. . . . . . . . 9 ⊢ (𝑧 = (𝐻 “ 𝑥) → (∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅ ↔ ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅))
24	20, 23	imbi12d 347	. . . . . . . 8 ⊢ (𝑧 = (𝐻 “ 𝑥) → (((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅) ↔ (((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
25	24	spcgv 3551	. . . . . . 7 ⊢ ((𝐻 “ 𝑥) ∈ V → (∀𝑧((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅) → (((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
26	17, 25	syl 18	. . . . . 6 ⊢ (𝜑 → (∀𝑧((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅) → (((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
27	16, 26	biimtrid 245	. . . . 5 ⊢ (𝜑 → (𝑆 Fr 𝐵 → (((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
28	15, 27	syl5d 74	. . . 4 ⊢ (𝜑 → (𝑆 Fr 𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
29	3	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → 𝐻:𝐴⟶𝐵)
30	29	ffund 6706	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → Fun 𝐻)
31		simpl 488	. . . . . . . . . 10 ⊢ ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → 𝑤 ∈ (𝐻 “ 𝑥))
32		fvelima 6942	. . . . . . . . . 10 ⊢ ((Fun 𝐻 ∧ 𝑤 ∈ (𝐻 “ 𝑥)) → ∃𝑦 ∈ 𝑥 (𝐻‘𝑦) = 𝑤)
33	30, 31, 32	syl2an 608	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → ∃𝑦 ∈ 𝑥 (𝐻‘𝑦) = 𝑤)
34		sneq 4594	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = (𝐻‘𝑦) → {𝑤} = {(𝐻‘𝑦)})
35	34	eqcoms 2769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐻‘𝑦) = 𝑤 → {𝑤} = {(𝐻‘𝑦)})
36	35	imaeq2d 6054	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐻‘𝑦) = 𝑤 → (◡𝑆 “ {𝑤}) = (◡𝑆 “ {(𝐻‘𝑦)}))
37	36	ineq2d 4166	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐻‘𝑦) = 𝑤 → ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})))
38	37	eqeq1d 2763	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻‘𝑦) = 𝑤 → (((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ ↔ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ∅))
39	38	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐻‘𝑦) = 𝑤 → (((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ → ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ∅))
40		ssel 3925	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ⊆ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴))
41	40	imdistani 579	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥) → (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐴))
42		relpmin 45894	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ∅ → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
43	1, 41, 42	syl2an 608	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥)) → (((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ∅ → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
44	39, 43	sylan9r 518	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥)) ∧ (𝐻‘𝑦) = 𝑤) → (((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
45	44	adantld 496	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥)) ∧ (𝐻‘𝑦) = 𝑤) → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
46	45	exp42 441	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ⊆ 𝐴 → (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))))
47	46	imp 412	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))))
48	47	com3l 90	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → ((𝜑 ∧ 𝑥 ⊆ 𝐴) → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))))
49	48	com4t 94	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))))
50	49	imp 412	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
51	50	reximdvai 3174	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → (∃𝑦 ∈ 𝑥 (𝐻‘𝑦) = 𝑤 → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
52	33, 51	mpd 16	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)
53	52	rexlimdvaa 3165	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
54	53	ex 418	. . . . . 6 ⊢ (𝜑 → (𝑥 ⊆ 𝐴 → (∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
55	54	adantrd 497	. . . . 5 ⊢ (𝜑 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
56	55	a2d 30	. . . 4 ⊢ (𝜑 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
57	28, 56	syld 48	. . 3 ⊢ (𝜑 → (𝑆 Fr 𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
58	57	alrimdv 1962	. 2 ⊢ (𝜑 → (𝑆 Fr 𝐵 → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
59		dffr3 6093	. 2 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
60	58, 59	imbitrrdi 255	1 ⊢ (𝜑 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2956  ∃wrex 3087  Vcvv 3451   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  {csn 4584   Fr wfr 5601  ^◡ccnv 5650   “ cima 5654  Fun wfun 6525   Fn wfn 6526  ⟶wf 6527  ‘cfv 6531   RelPres wrelp 45884

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-fr 5604  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-relp 45885

This theorem is used by:  relpfr  45896