Theorem isoselem 6911

Description: Lemma for isose 6913. (Contributed by Mario Carneiro, 23-Jun-2015.)

Hypotheses

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

Assertion

Ref	Expression
isoselem	⊢ (𝜑 → (𝑅 Se 𝐴 → 𝑆 Se 𝐵))

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

Proof of Theorem isoselem

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

Step	Hyp	Ref	Expression
1		dfse2 5797	. . . . . . . . 9 ⊢ (𝑅 Se 𝐴 ↔ ∀𝑧 ∈ 𝐴 (𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V)
2	1	biimpi 208	. . . . . . . 8 ⊢ (𝑅 Se 𝐴 → ∀𝑧 ∈ 𝐴 (𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V)
3	2	r19.21bi 3152	. . . . . . 7 ⊢ ((𝑅 Se 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V)
4	3	expcom 406	. . . . . 6 ⊢ (𝑧 ∈ 𝐴 → (𝑅 Se 𝐴 → (𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V))
5	4	adantl 474	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑅 Se 𝐴 → (𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V))
6		imaeq2 5760	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐴 ∩ (◡𝑅 “ {𝑧})) → (𝐻 “ 𝑥) = (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))))
7	6	eleq1d 2844	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴 ∩ (◡𝑅 “ {𝑧})) → ((𝐻 “ 𝑥) ∈ V ↔ (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) ∈ V))
8	7	imbi2d 333	. . . . . . . . 9 ⊢ (𝑥 = (𝐴 ∩ (◡𝑅 “ {𝑧})) → ((𝜑 → (𝐻 “ 𝑥) ∈ V) ↔ (𝜑 → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) ∈ V)))
9		isofrlem.2	. . . . . . . . 9 ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)
10	8, 9	vtoclg 3480	. . . . . . . 8 ⊢ ((𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V → (𝜑 → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) ∈ V))
11	10	com12 32	. . . . . . 7 ⊢ (𝜑 → ((𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) ∈ V))
12	11	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) ∈ V))
13		isofrlem.1	. . . . . . . 8 ⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))
14		isoini 6908	. . . . . . . 8 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑧 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})))
15	13, 14	sylan 572	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})))
16	15	eleq1d 2844	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) ∈ V ↔ (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V))
17	12, 16	sylibd 231	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V → (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V))
18	5, 17	syld 47	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑅 Se 𝐴 → (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V))
19	18	ralrimdva 3133	. . 3 ⊢ (𝜑 → (𝑅 Se 𝐴 → ∀𝑧 ∈ 𝐴 (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V))
20		isof1o 6893	. . . . 5 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)
21		f1ofn 6439	. . . . 5 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → 𝐻 Fn 𝐴)
22		sneq 4445	. . . . . . . . 9 ⊢ (𝑦 = (𝐻‘𝑧) → {𝑦} = {(𝐻‘𝑧)})
23	22	imaeq2d 5764	. . . . . . . 8 ⊢ (𝑦 = (𝐻‘𝑧) → (◡𝑆 “ {𝑦}) = (◡𝑆 “ {(𝐻‘𝑧)}))
24	23	ineq2d 4071	. . . . . . 7 ⊢ (𝑦 = (𝐻‘𝑧) → (𝐵 ∩ (◡𝑆 “ {𝑦})) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})))
25	24	eleq1d 2844	. . . . . 6 ⊢ (𝑦 = (𝐻‘𝑧) → ((𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V ↔ (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V))
26	25	ralrn 6673	. . . . 5 ⊢ (𝐻 Fn 𝐴 → (∀𝑦 ∈ ran 𝐻(𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V ↔ ∀𝑧 ∈ 𝐴 (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V))
27	13, 20, 21, 26	4syl 19	. . . 4 ⊢ (𝜑 → (∀𝑦 ∈ ran 𝐻(𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V ↔ ∀𝑧 ∈ 𝐴 (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V))
28		f1ofo 6445	. . . . . 6 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → 𝐻:𝐴–onto→𝐵)
29		forn 6416	. . . . . 6 ⊢ (𝐻:𝐴–onto→𝐵 → ran 𝐻 = 𝐵)
30	13, 20, 28, 29	4syl 19	. . . . 5 ⊢ (𝜑 → ran 𝐻 = 𝐵)
31	30	raleqdv 3349	. . . 4 ⊢ (𝜑 → (∀𝑦 ∈ ran 𝐻(𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V ↔ ∀𝑦 ∈ 𝐵 (𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V))
32	27, 31	bitr3d 273	. . 3 ⊢ (𝜑 → (∀𝑧 ∈ 𝐴 (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V ↔ ∀𝑦 ∈ 𝐵 (𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V))
33	19, 32	sylibd 231	. 2 ⊢ (𝜑 → (𝑅 Se 𝐴 → ∀𝑦 ∈ 𝐵 (𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V))
34		dfse2 5797	. 2 ⊢ (𝑆 Se 𝐵 ↔ ∀𝑦 ∈ 𝐵 (𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V)
35	33, 34	syl6ibr 244	1 ⊢ (𝜑 → (𝑅 Se 𝐴 → 𝑆 Se 𝐵))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507   ∈ wcel 2048  ∀wral 3082  Vcvv 3409   ∩ cin 3824  {csn 4435   Se wse 5357  ^◡ccnv 5399  ran crn 5401   “ cima 5403   Fn wfn 6177  –onto→wfo 6180  –1-1-onto→wf1o 6181  ‘cfv 6182   Isom wiso 6183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pr 5180

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3678  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5305  df-se 5360  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191

This theorem is referenced by:  isose  6913