Metamath Proof Explorer

Theorem isofrlem

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

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

Proof

Step Hyp Ref Expression
1 isofrlem.1 ⊢ ( 𝜑 → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
2 isofrlem.2 ⊢ ( 𝜑 → ( 𝐻 “ 𝑥 ) ∈ V )
3 isof1o ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
4 1 3 syl ⊢ ( 𝜑 → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
5 f1ofn ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 Fn 𝐴 )
6 n0 ⊢ ( 𝑥 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑥 )
7 fnfvima ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ( 𝐻 ‘ 𝑦 ) ∈ ( 𝐻 “ 𝑥 ) )
8 7 ne0d ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ( 𝐻 “ 𝑥 ) ≠ ∅ )
9 8 3expia ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑦 ∈ 𝑥 → ( 𝐻 “ 𝑥 ) ≠ ∅ ) )
10 9 exlimdv ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → ( ∃ 𝑦 𝑦 ∈ 𝑥 → ( 𝐻 “ 𝑥 ) ≠ ∅ ) )
11 6 10 biimtrid ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑥 ≠ ∅ → ( 𝐻 “ 𝑥 ) ≠ ∅ ) )
12 11 expimpd ⊢ ( 𝐻 Fn 𝐴 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( 𝐻 “ 𝑥 ) ≠ ∅ ) )
13 5 12 syl ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( 𝐻 “ 𝑥 ) ≠ ∅ ) )
14 f1ofo ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 –onto→ 𝐵 )
15 imassrn ⊢ ( 𝐻 “ 𝑥 ) ⊆ ran 𝐻
16 forn ⊢ ( 𝐻 : 𝐴 –onto→ 𝐵 → ran 𝐻 = 𝐵 )
17 15 16 sseqtrid ⊢ ( 𝐻 : 𝐴 –onto→ 𝐵 → ( 𝐻 “ 𝑥 ) ⊆ 𝐵 )
18 14 17 syl ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ( 𝐻 “ 𝑥 ) ⊆ 𝐵 )
19 13 18 jctild ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐻 “ 𝑥 ) ≠ ∅ ) ) )
20 4 19 syl ⊢ ( 𝜑 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐻 “ 𝑥 ) ≠ ∅ ) ) )
21 dffr3 ⊢ ( 𝑆 Fr 𝐵 ↔ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ( 𝑧 ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) )
22 sseq1 ⊢ ( 𝑧 = ( 𝐻 “ 𝑥 ) → ( 𝑧 ⊆ 𝐵 ↔ ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ) )
23 neeq1 ⊢ ( 𝑧 = ( 𝐻 “ 𝑥 ) → ( 𝑧 ≠ ∅ ↔ ( 𝐻 “ 𝑥 ) ≠ ∅ ) )
24 22 23 anbi12d ⊢ ( 𝑧 = ( 𝐻 “ 𝑥 ) → ( ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅ ) ↔ ( ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐻 “ 𝑥 ) ≠ ∅ ) ) )
25 ineq1 ⊢ ( 𝑧 = ( 𝐻 “ 𝑥 ) → ( 𝑧 ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) )
26 25 eqeq1d ⊢ ( 𝑧 = ( 𝐻 “ 𝑥 ) → ( ( 𝑧 ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ↔ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) )
27 26 rexeqbi1dv ⊢ ( 𝑧 = ( 𝐻 “ 𝑥 ) → ( ∃ 𝑤 ∈ 𝑧 ( 𝑧 ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ↔ ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) )
28 24 27 imbi12d ⊢ ( 𝑧 = ( 𝐻 “ 𝑥 ) → ( ( ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ( 𝑧 ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ↔ ( ( ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐻 “ 𝑥 ) ≠ ∅ ) → ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) )
29 28 spcgv ⊢ ( ( 𝐻 “ 𝑥 ) ∈ V → ( ∀ 𝑧 ( ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ( 𝑧 ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( ( ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐻 “ 𝑥 ) ≠ ∅ ) → ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) )
30 2 29 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ( ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ( 𝑧 ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( ( ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐻 “ 𝑥 ) ≠ ∅ ) → ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) )
31 21 30 biimtrid ⊢ ( 𝜑 → ( 𝑆 Fr 𝐵 → ( ( ( 𝐻 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐻 “ 𝑥 ) ≠ ∅ ) → ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) )
32 20 31 syl5d ⊢ ( 𝜑 → ( 𝑆 Fr 𝐵 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) )
33 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
34 f1ofun ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → Fun 𝐻 )
35 33 34 syl ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → Fun 𝐻 )
36 simpl ⊢ ( ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → 𝑤 ∈ ( 𝐻 “ 𝑥 ) )
37 fvelima ⊢ ( ( Fun 𝐻 ∧ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ) → ∃ 𝑦 ∈ 𝑥 ( 𝐻 ‘ 𝑦 ) = 𝑤 )
38 35 36 37 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) → ∃ 𝑦 ∈ 𝑥 ( 𝐻 ‘ 𝑦 ) = 𝑤 )
39 simpr ⊢ ( ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ )
40 ssel ⊢ ( 𝑥 ⊆ 𝐴 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴 ) )
41 40 imdistani ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐴 ) )
42 isomin ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ↔ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑦 ) } ) ) = ∅ ) )
43 1 41 42 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) → ( ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ↔ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑦 ) } ) ) = ∅ ) )
44 sneq ⊢ ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → { ( 𝐻 ‘ 𝑦 ) } = { 𝑤 } )
45 44 imaeq2d ⊢ ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑦 ) } ) = ( ◡ 𝑆 “ { 𝑤 } ) )
46 45 ineq2d ⊢ ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑦 ) } ) ) = ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) )
47 46 eqeq1d ⊢ ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑦 ) } ) ) = ∅ ↔ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) )
48 43 47 sylan9bb ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝐻 ‘ 𝑦 ) = 𝑤 ) → ( ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ↔ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) )
49 39 48 imbitrrid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝐻 ‘ 𝑦 ) = 𝑤 ) → ( ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )
50 49 exp42 ⊢ ( 𝜑 → ( 𝑥 ⊆ 𝐴 → ( 𝑦 ∈ 𝑥 → ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) ) ) )
51 50 imp ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑦 ∈ 𝑥 → ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) ) )
52 51 com3l ⊢ ( 𝑦 ∈ 𝑥 → ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ( ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) ) )
53 52 com4t ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ( ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( 𝑦 ∈ 𝑥 → ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) ) )
54 53 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) → ( 𝑦 ∈ 𝑥 → ( ( 𝐻 ‘ 𝑦 ) = 𝑤 → ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) )
55 54 reximdvai ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) → ( ∃ 𝑦 ∈ 𝑥 ( 𝐻 ‘ 𝑦 ) = 𝑤 → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )
56 38 55 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑤 ∈ ( 𝐻 “ 𝑥 ) ∧ ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ )
57 56 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ( ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )
58 57 ex ⊢ ( 𝜑 → ( 𝑥 ⊆ 𝐴 → ( ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) )
59 58 adantrd ⊢ ( 𝜑 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) )
60 59 a2d ⊢ ( 𝜑 → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑤 ∈ ( 𝐻 “ 𝑥 ) ( ( 𝐻 “ 𝑥 ) ∩ ( ◡ 𝑆 “ { 𝑤 } ) ) = ∅ ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) )
61 32 60 syld ⊢ ( 𝜑 → ( 𝑆 Fr 𝐵 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) )
62 61 alrimdv ⊢ ( 𝜑 → ( 𝑆 Fr 𝐵 → ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) ) )
63 dffr3 ⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ∅ ) )
64 62 63 imbitrrdi ⊢ ( 𝜑 → ( 𝑆 Fr 𝐵 → 𝑅 Fr 𝐴 ) )