Theorem isofrlem 7315

Description: Lemma for isofr 7317. (Contributed by NM, 29-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.)

Hypotheses

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

Assertion

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

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

Proof of Theorem isofrlem

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

Step	Hyp	Ref	Expression
1		isofrlem.1	. . . . . . 7 ⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))
2		isof1o 7298	. . . . . . 7 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)
3	1, 2	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻:𝐴–1-1-onto→𝐵)
4		f1ofn 6801	. . . . . . . 8 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → 𝐻 Fn 𝐴)
5		n0 4316	. . . . . . . . . 10 ⊢ (𝑥 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝑥)
6		fnfvima 7207	. . . . . . . . . . . . 13 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥) → (𝐻‘𝑦) ∈ (𝐻 “ 𝑥))
7	6	ne0d 4305	. . . . . . . . . . . 12 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥) → (𝐻 “ 𝑥) ≠ ∅)
8	7	3expia 1121	. . . . . . . . . . 11 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴) → (𝑦 ∈ 𝑥 → (𝐻 “ 𝑥) ≠ ∅))
9	8	exlimdv 1933	. . . . . . . . . 10 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 𝑦 ∈ 𝑥 → (𝐻 “ 𝑥) ≠ ∅))
10	5, 9	biimtrid 242	. . . . . . . . 9 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴) → (𝑥 ≠ ∅ → (𝐻 “ 𝑥) ≠ ∅))
11	10	expimpd 453	. . . . . . . 8 ⊢ (𝐻 Fn 𝐴 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝐻 “ 𝑥) ≠ ∅))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (𝐻 “ 𝑥) ≠ ∅))
13		f1ofo 6807	. . . . . . . 8 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → 𝐻:𝐴–onto→𝐵)
14		imassrn 6042	. . . . . . . . 9 ⊢ (𝐻 “ 𝑥) ⊆ ran 𝐻
15		forn 6775	. . . . . . . . 9 ⊢ (𝐻:𝐴–onto→𝐵 → ran 𝐻 = 𝐵)
16	14, 15	sseqtrid 3989	. . . . . . . 8 ⊢ (𝐻:𝐴–onto→𝐵 → (𝐻 “ 𝑥) ⊆ 𝐵)
17	13, 16	syl 17	. . . . . . 7 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → (𝐻 “ 𝑥) ⊆ 𝐵)
18	12, 17	jctild 525	. . . . . 6 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅)))
19	3, 18	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅)))
20		dffr3 6070	. . . . . 6 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑧((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅))
21		isofrlem.2	. . . . . . 7 ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)
22		sseq1 3972	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 “ 𝑥) → (𝑧 ⊆ 𝐵 ↔ (𝐻 “ 𝑥) ⊆ 𝐵))
23		neeq1 2987	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 “ 𝑥) → (𝑧 ≠ ∅ ↔ (𝐻 “ 𝑥) ≠ ∅))
24	22, 23	anbi12d 632	. . . . . . . . 9 ⊢ (𝑧 = (𝐻 “ 𝑥) → ((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) ↔ ((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅)))
25		ineq1 4176	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐻 “ 𝑥) → (𝑧 ∩ (◡𝑆 “ {𝑤})) = ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})))
26	25	eqeq1d 2731	. . . . . . . . . 10 ⊢ (𝑧 = (𝐻 “ 𝑥) → ((𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅ ↔ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅))
27	26	rexeqbi1dv 3312	. . . . . . . . 9 ⊢ (𝑧 = (𝐻 “ 𝑥) → (∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅ ↔ ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅))
28	24, 27	imbi12d 344	. . . . . . . 8 ⊢ (𝑧 = (𝐻 “ 𝑥) → (((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅) ↔ (((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
29	28	spcgv 3562	. . . . . . 7 ⊢ ((𝐻 “ 𝑥) ∈ V → (∀𝑧((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅) → (((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
30	21, 29	syl 17	. . . . . 6 ⊢ (𝜑 → (∀𝑧((𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 (𝑧 ∩ (◡𝑆 “ {𝑤})) = ∅) → (((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
31	20, 30	biimtrid 242	. . . . 5 ⊢ (𝜑 → (𝑆 Fr 𝐵 → (((𝐻 “ 𝑥) ⊆ 𝐵 ∧ (𝐻 “ 𝑥) ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
32	19, 31	syl5d 73	. . . 4 ⊢ (𝜑 → (𝑆 Fr 𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)))
33	3	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → 𝐻:𝐴–1-1-onto→𝐵)
34		f1ofun 6802	. . . . . . . . . . 11 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → Fun 𝐻)
35	33, 34	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → Fun 𝐻)
36		simpl 482	. . . . . . . . . 10 ⊢ ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → 𝑤 ∈ (𝐻 “ 𝑥))
37		fvelima 6926	. . . . . . . . . 10 ⊢ ((Fun 𝐻 ∧ 𝑤 ∈ (𝐻 “ 𝑥)) → ∃𝑦 ∈ 𝑥 (𝐻‘𝑦) = 𝑤)
38	35, 36, 37	syl2an 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → ∃𝑦 ∈ 𝑥 (𝐻‘𝑦) = 𝑤)
39		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)
40		ssel 3940	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ⊆ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴))
41	40	imdistani 568	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥) → (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐴))
42		isomin 7312	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅ ↔ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ∅))
43	1, 41, 42	syl2an 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥)) → ((𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅ ↔ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ∅))
44		sneq 4599	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐻‘𝑦) = 𝑤 → {(𝐻‘𝑦)} = {𝑤})
45	44	imaeq2d 6031	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐻‘𝑦) = 𝑤 → (◡𝑆 “ {(𝐻‘𝑦)}) = (◡𝑆 “ {𝑤}))
46	45	ineq2d 4183	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻‘𝑦) = 𝑤 → ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})))
47	46	eqeq1d 2731	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐻‘𝑦) = 𝑤 → (((𝐻 “ 𝑥) ∩ (◡𝑆 “ {(𝐻‘𝑦)})) = ∅ ↔ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅))
48	43, 47	sylan9bb 509	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥)) ∧ (𝐻‘𝑦) = 𝑤) → ((𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅ ↔ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅))
49	39, 48	imbitrrid 246	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥)) ∧ (𝐻‘𝑦) = 𝑤) → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
50	49	exp42 435	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ⊆ 𝐴 → (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))))
51	50	imp 406	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))))
52	51	com3l 89	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → ((𝜑 ∧ 𝑥 ⊆ 𝐴) → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))))
53	52	com4t 93	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → ((𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))))
54	53	imp 406	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → (𝑦 ∈ 𝑥 → ((𝐻‘𝑦) = 𝑤 → (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
55	54	reximdvai 3144	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → (∃𝑦 ∈ 𝑥 (𝐻‘𝑦) = 𝑤 → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
56	38, 55	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ (𝑤 ∈ (𝐻 “ 𝑥) ∧ ((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅)) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)
57	56	rexlimdvaa 3135	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
58	57	ex 412	. . . . . 6 ⊢ (𝜑 → (𝑥 ⊆ 𝐴 → (∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
59	58	adantrd 491	. . . . 5 ⊢ (𝜑 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅ → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
60	59	a2d 29	. . . 4 ⊢ (𝜑 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑤 ∈ (𝐻 “ 𝑥)((𝐻 “ 𝑥) ∩ (◡𝑆 “ {𝑤})) = ∅) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
61	32, 60	syld 47	. . 3 ⊢ (𝜑 → (𝑆 Fr 𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
62	61	alrimdv 1929	. 2 ⊢ (𝜑 → (𝑆 Fr 𝐵 → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)))
63		dffr3 6070	. 2 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
64	62, 63	imbitrrdi 252	1 ⊢ (𝜑 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925  ∃wrex 3053  Vcvv 3447   ∩ cin 3913   ⊆ wss 3914  ∅c0 4296  {csn 4589   Fr wfr 5588  ^◡ccnv 5637  ran crn 5639   “ cima 5641  Fun wfun 6505   Fn wfn 6506  –onto→wfo 6509  –1-1-onto→wf1o 6510  ‘cfv 6511   Isom wiso 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-fr 5591  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520

This theorem is referenced by:  isofr  7317  isofr2  7319  isowe2  7325