Metamath Proof Explorer

Theorem f1oweALT

Description: Alternate proof of f1owe , more direct since not using the isomorphism predicate, but requiring ax-un . (Contributed by NM, 4-Mar-1997) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis f1oweALT.1 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) }
Assertion f1oweALT ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( 𝑆 We 𝐵 → 𝑅 We 𝐴 ) )

Proof

Step Hyp Ref Expression
1 f1oweALT.1 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) }
2 f1ofo ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –onto→ 𝐵 )
3 df-fo ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) )
4 freq2 ⊢ ( ran 𝐹 = 𝐵 → ( 𝑆 Fr ran 𝐹 ↔ 𝑆 Fr 𝐵 ) )
5 4 biimprd ⊢ ( ran 𝐹 = 𝐵 → ( 𝑆 Fr 𝐵 → 𝑆 Fr ran 𝐹 ) )
6 df-fn ⊢ ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) )
7 df-fr ⊢ ( 𝑆 Fr ran 𝐹 ↔ ∀ 𝑤 ( ( 𝑤 ⊆ ran 𝐹 ∧ 𝑤 ≠ ∅ ) → ∃ 𝑢 ∈ 𝑤 ∀ 𝑓 ∈ 𝑤 ¬ 𝑓 𝑆 𝑢 ) )
8 vex ⊢ 𝑧 ∈ V
9 8 funimaex ⊢ ( Fun 𝐹 → ( 𝐹 “ 𝑧 ) ∈ V )
10 n0 ⊢ ( 𝑧 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝑧 )
11 funfvima2 ⊢ ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) → ( 𝑤 ∈ 𝑧 → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑧 ) ) )
12 ne0i ⊢ ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ 𝑧 ) → ( 𝐹 “ 𝑧 ) ≠ ∅ )
13 11 12 syl6 ⊢ ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) → ( 𝑤 ∈ 𝑧 → ( 𝐹 “ 𝑧 ) ≠ ∅ ) )
14 13 exlimdv ⊢ ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) → ( ∃ 𝑤 𝑤 ∈ 𝑧 → ( 𝐹 “ 𝑧 ) ≠ ∅ ) )
15 10 14 syl5bi ⊢ ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) → ( 𝑧 ≠ ∅ → ( 𝐹 “ 𝑧 ) ≠ ∅ ) )
16 15 imp ⊢ ( ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) ∧ 𝑧 ≠ ∅ ) → ( 𝐹 “ 𝑧 ) ≠ ∅ )
17 imassrn ⊢ ( 𝐹 “ 𝑧 ) ⊆ ran 𝐹
18 16 17 jctil ⊢ ( ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) ∧ 𝑧 ≠ ∅ ) → ( ( 𝐹 “ 𝑧 ) ⊆ ran 𝐹 ∧ ( 𝐹 “ 𝑧 ) ≠ ∅ ) )
19 sseq1 ⊢ ( 𝑤 = ( 𝐹 “ 𝑧 ) → ( 𝑤 ⊆ ran 𝐹 ↔ ( 𝐹 “ 𝑧 ) ⊆ ran 𝐹 ) )
20 neeq1 ⊢ ( 𝑤 = ( 𝐹 “ 𝑧 ) → ( 𝑤 ≠ ∅ ↔ ( 𝐹 “ 𝑧 ) ≠ ∅ ) )
21 19 20 anbi12d ⊢ ( 𝑤 = ( 𝐹 “ 𝑧 ) → ( ( 𝑤 ⊆ ran 𝐹 ∧ 𝑤 ≠ ∅ ) ↔ ( ( 𝐹 “ 𝑧 ) ⊆ ran 𝐹 ∧ ( 𝐹 “ 𝑧 ) ≠ ∅ ) ) )
22 raleq ⊢ ( 𝑤 = ( 𝐹 “ 𝑧 ) → ( ∀ 𝑓 ∈ 𝑤 ¬ 𝑓 𝑆 𝑢 ↔ ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) )
23 22 rexeqbi1dv ⊢ ( 𝑤 = ( 𝐹 “ 𝑧 ) → ( ∃ 𝑢 ∈ 𝑤 ∀ 𝑓 ∈ 𝑤 ¬ 𝑓 𝑆 𝑢 ↔ ∃ 𝑢 ∈ ( 𝐹 “ 𝑧 ) ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) )
24 21 23 imbi12d ⊢ ( 𝑤 = ( 𝐹 “ 𝑧 ) → ( ( ( 𝑤 ⊆ ran 𝐹 ∧ 𝑤 ≠ ∅ ) → ∃ 𝑢 ∈ 𝑤 ∀ 𝑓 ∈ 𝑤 ¬ 𝑓 𝑆 𝑢 ) ↔ ( ( ( 𝐹 “ 𝑧 ) ⊆ ran 𝐹 ∧ ( 𝐹 “ 𝑧 ) ≠ ∅ ) → ∃ 𝑢 ∈ ( 𝐹 “ 𝑧 ) ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) ) )
25 24 spcgv ⊢ ( ( 𝐹 “ 𝑧 ) ∈ V → ( ∀ 𝑤 ( ( 𝑤 ⊆ ran 𝐹 ∧ 𝑤 ≠ ∅ ) → ∃ 𝑢 ∈ 𝑤 ∀ 𝑓 ∈ 𝑤 ¬ 𝑓 𝑆 𝑢 ) → ( ( ( 𝐹 “ 𝑧 ) ⊆ ran 𝐹 ∧ ( 𝐹 “ 𝑧 ) ≠ ∅ ) → ∃ 𝑢 ∈ ( 𝐹 “ 𝑧 ) ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) ) )
26 18 25 syl7 ⊢ ( ( 𝐹 “ 𝑧 ) ∈ V → ( ∀ 𝑤 ( ( 𝑤 ⊆ ran 𝐹 ∧ 𝑤 ≠ ∅ ) → ∃ 𝑢 ∈ 𝑤 ∀ 𝑓 ∈ 𝑤 ¬ 𝑓 𝑆 𝑢 ) → ( ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) ∧ 𝑧 ≠ ∅ ) → ∃ 𝑢 ∈ ( 𝐹 “ 𝑧 ) ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) ) )
27 9 26 syl ⊢ ( Fun 𝐹 → ( ∀ 𝑤 ( ( 𝑤 ⊆ ran 𝐹 ∧ 𝑤 ≠ ∅ ) → ∃ 𝑢 ∈ 𝑤 ∀ 𝑓 ∈ 𝑤 ¬ 𝑓 𝑆 𝑢 ) → ( ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) ∧ 𝑧 ≠ ∅ ) → ∃ 𝑢 ∈ ( 𝐹 “ 𝑧 ) ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) ) )
28 7 27 syl5bi ⊢ ( Fun 𝐹 → ( 𝑆 Fr ran 𝐹 → ( ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) ∧ 𝑧 ≠ ∅ ) → ∃ 𝑢 ∈ ( 𝐹 “ 𝑧 ) ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) ) )
29 28 com23 ⊢ ( Fun 𝐹 → ( ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) ∧ 𝑧 ≠ ∅ ) → ( 𝑆 Fr ran 𝐹 → ∃ 𝑢 ∈ ( 𝐹 “ 𝑧 ) ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) ) )
30 29 expd ⊢ ( Fun 𝐹 → ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) → ( 𝑧 ≠ ∅ → ( 𝑆 Fr ran 𝐹 → ∃ 𝑢 ∈ ( 𝐹 “ 𝑧 ) ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) ) ) )
31 30 anabsi5 ⊢ ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) → ( 𝑧 ≠ ∅ → ( 𝑆 Fr ran 𝐹 → ∃ 𝑢 ∈ ( 𝐹 “ 𝑧 ) ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) ) )
32 31 impd ⊢ ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) → ( ( 𝑧 ≠ ∅ ∧ 𝑆 Fr ran 𝐹 ) → ∃ 𝑢 ∈ ( 𝐹 “ 𝑧 ) ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) )
33 fores ⊢ ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝑧 ) : 𝑧 –onto→ ( 𝐹 “ 𝑧 ) )
34 vex ⊢ 𝑣 ∈ V
35 vex ⊢ 𝑤 ∈ V
36 fveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑣 ) )
37 36 breq1d ⊢ ( 𝑥 = 𝑣 → ( ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑣 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
38 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) )
39 38 breq2d ⊢ ( 𝑦 = 𝑤 → ( ( 𝐹 ‘ 𝑣 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑣 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) )
40 34 35 37 39 1 brab ⊢ ( 𝑣 𝑅 𝑤 ↔ ( 𝐹 ‘ 𝑣 ) 𝑆 ( 𝐹 ‘ 𝑤 ) )
41 fvres ⊢ ( 𝑣 ∈ 𝑧 → ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑣 ) = ( 𝐹 ‘ 𝑣 ) )
42 fvres ⊢ ( 𝑤 ∈ 𝑧 → ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
43 41 42 breqan12rd ⊢ ( ( 𝑤 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧 ) → ( ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑣 ) 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑣 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) )
44 40 43 bitr4id ⊢ ( ( 𝑤 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧 ) → ( 𝑣 𝑅 𝑤 ↔ ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑣 ) 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ) )
45 44 notbid ⊢ ( ( 𝑤 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧 ) → ( ¬ 𝑣 𝑅 𝑤 ↔ ¬ ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑣 ) 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ) )
46 45 ralbidva ⊢ ( 𝑤 ∈ 𝑧 → ( ∀ 𝑣 ∈ 𝑧 ¬ 𝑣 𝑅 𝑤 ↔ ∀ 𝑣 ∈ 𝑧 ¬ ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑣 ) 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ) )
47 46 rexbiia ⊢ ( ∃ 𝑤 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ¬ 𝑣 𝑅 𝑤 ↔ ∃ 𝑤 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ¬ ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑣 ) 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) )
48 breq1 ⊢ ( ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑣 ) = 𝑓 → ( ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑣 ) 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ↔ 𝑓 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ) )
49 48 notbid ⊢ ( ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑣 ) = 𝑓 → ( ¬ ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑣 ) 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ↔ ¬ 𝑓 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ) )
50 49 cbvfo ⊢ ( ( 𝐹 ↾ 𝑧 ) : 𝑧 –onto→ ( 𝐹 “ 𝑧 ) → ( ∀ 𝑣 ∈ 𝑧 ¬ ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑣 ) 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ↔ ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ) )
51 50 rexbidv ⊢ ( ( 𝐹 ↾ 𝑧 ) : 𝑧 –onto→ ( 𝐹 “ 𝑧 ) → ( ∃ 𝑤 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ¬ ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑣 ) 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ↔ ∃ 𝑤 ∈ 𝑧 ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ) )
52 breq2 ⊢ ( ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) = 𝑢 → ( 𝑓 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ↔ 𝑓 𝑆 𝑢 ) )
53 52 notbid ⊢ ( ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) = 𝑢 → ( ¬ 𝑓 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ↔ ¬ 𝑓 𝑆 𝑢 ) )
54 53 ralbidv ⊢ ( ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) = 𝑢 → ( ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ↔ ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) )
55 54 cbvexfo ⊢ ( ( 𝐹 ↾ 𝑧 ) : 𝑧 –onto→ ( 𝐹 “ 𝑧 ) → ( ∃ 𝑤 ∈ 𝑧 ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ↔ ∃ 𝑢 ∈ ( 𝐹 “ 𝑧 ) ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) )
56 51 55 bitrd ⊢ ( ( 𝐹 ↾ 𝑧 ) : 𝑧 –onto→ ( 𝐹 “ 𝑧 ) → ( ∃ 𝑤 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ¬ ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑣 ) 𝑆 ( ( 𝐹 ↾ 𝑧 ) ‘ 𝑤 ) ↔ ∃ 𝑢 ∈ ( 𝐹 “ 𝑧 ) ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) )
57 47 56 syl5bb ⊢ ( ( 𝐹 ↾ 𝑧 ) : 𝑧 –onto→ ( 𝐹 “ 𝑧 ) → ( ∃ 𝑤 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ¬ 𝑣 𝑅 𝑤 ↔ ∃ 𝑢 ∈ ( 𝐹 “ 𝑧 ) ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) )
58 33 57 syl ⊢ ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) → ( ∃ 𝑤 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ¬ 𝑣 𝑅 𝑤 ↔ ∃ 𝑢 ∈ ( 𝐹 “ 𝑧 ) ∀ 𝑓 ∈ ( 𝐹 “ 𝑧 ) ¬ 𝑓 𝑆 𝑢 ) )
59 32 58 sylibrd ⊢ ( ( Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹 ) → ( ( 𝑧 ≠ ∅ ∧ 𝑆 Fr ran 𝐹 ) → ∃ 𝑤 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ¬ 𝑣 𝑅 𝑤 ) )
60 59 exp4b ⊢ ( Fun 𝐹 → ( 𝑧 ⊆ dom 𝐹 → ( 𝑧 ≠ ∅ → ( 𝑆 Fr ran 𝐹 → ∃ 𝑤 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ¬ 𝑣 𝑅 𝑤 ) ) ) )
61 60 com34 ⊢ ( Fun 𝐹 → ( 𝑧 ⊆ dom 𝐹 → ( 𝑆 Fr ran 𝐹 → ( 𝑧 ≠ ∅ → ∃ 𝑤 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ¬ 𝑣 𝑅 𝑤 ) ) ) )
62 61 com23 ⊢ ( Fun 𝐹 → ( 𝑆 Fr ran 𝐹 → ( 𝑧 ⊆ dom 𝐹 → ( 𝑧 ≠ ∅ → ∃ 𝑤 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ¬ 𝑣 𝑅 𝑤 ) ) ) )
63 62 imp4a ⊢ ( Fun 𝐹 → ( 𝑆 Fr ran 𝐹 → ( ( 𝑧 ⊆ dom 𝐹 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ¬ 𝑣 𝑅 𝑤 ) ) )
64 63 alrimdv ⊢ ( Fun 𝐹 → ( 𝑆 Fr ran 𝐹 → ∀ 𝑧 ( ( 𝑧 ⊆ dom 𝐹 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ¬ 𝑣 𝑅 𝑤 ) ) )
65 df-fr ⊢ ( 𝑅 Fr dom 𝐹 ↔ ∀ 𝑧 ( ( 𝑧 ⊆ dom 𝐹 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ¬ 𝑣 𝑅 𝑤 ) )
66 64 65 syl6ibr ⊢ ( Fun 𝐹 → ( 𝑆 Fr ran 𝐹 → 𝑅 Fr dom 𝐹 ) )
67 freq2 ⊢ ( dom 𝐹 = 𝐴 → ( 𝑅 Fr dom 𝐹 ↔ 𝑅 Fr 𝐴 ) )
68 67 biimpd ⊢ ( dom 𝐹 = 𝐴 → ( 𝑅 Fr dom 𝐹 → 𝑅 Fr 𝐴 ) )
69 66 68 sylan9 ⊢ ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) → ( 𝑆 Fr ran 𝐹 → 𝑅 Fr 𝐴 ) )
70 6 69 sylbi ⊢ ( 𝐹 Fn 𝐴 → ( 𝑆 Fr ran 𝐹 → 𝑅 Fr 𝐴 ) )
71 5 70 sylan9r ⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) → ( 𝑆 Fr 𝐵 → 𝑅 Fr 𝐴 ) )
72 3 71 sylbi ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝑆 Fr 𝐵 → 𝑅 Fr 𝐴 ) )
73 2 72 syl ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( 𝑆 Fr 𝐵 → 𝑅 Fr 𝐴 ) )
74 df-f1o ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) )
75 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
76 75 breq1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
77 fveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑣 ) )
78 77 breq2d ⊢ ( 𝑦 = 𝑣 → ( ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑣 ) ) )
79 35 34 76 78 1 brab ⊢ ( 𝑤 𝑅 𝑣 ↔ ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑣 ) )
80 79 a1i ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( 𝑤 𝑅 𝑣 ↔ ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑣 ) ) )
81 f1fveq ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) ↔ 𝑤 = 𝑣 ) )
82 81 bicomd ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( 𝑤 = 𝑣 ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) ) )
83 40 a1i ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( 𝑣 𝑅 𝑤 ↔ ( 𝐹 ‘ 𝑣 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) )
84 80 82 83 3orbi123d ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ( 𝑤 𝑅 𝑣 ∨ 𝑤 = 𝑣 ∨ 𝑣 𝑅 𝑤 ) ↔ ( ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑣 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) ) )
85 84 2ralbidva ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑤 𝑅 𝑣 ∨ 𝑤 = 𝑣 ∨ 𝑣 𝑅 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑣 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) ) )
86 breq1 ⊢ ( ( 𝐹 ‘ 𝑤 ) = 𝑢 → ( ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑣 ) ↔ 𝑢 𝑆 ( 𝐹 ‘ 𝑣 ) ) )
87 eqeq1 ⊢ ( ( 𝐹 ‘ 𝑤 ) = 𝑢 → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) ↔ 𝑢 = ( 𝐹 ‘ 𝑣 ) ) )
88 breq2 ⊢ ( ( 𝐹 ‘ 𝑤 ) = 𝑢 → ( ( 𝐹 ‘ 𝑣 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑣 ) 𝑆 𝑢 ) )
89 86 87 88 3orbi123d ⊢ ( ( 𝐹 ‘ 𝑤 ) = 𝑢 → ( ( ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑣 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) ↔ ( 𝑢 𝑆 ( 𝐹 ‘ 𝑣 ) ∨ 𝑢 = ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑣 ) 𝑆 𝑢 ) ) )
90 89 ralbidv ⊢ ( ( 𝐹 ‘ 𝑤 ) = 𝑢 → ( ∀ 𝑣 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑣 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) ↔ ∀ 𝑣 ∈ 𝐴 ( 𝑢 𝑆 ( 𝐹 ‘ 𝑣 ) ∨ 𝑢 = ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑣 ) 𝑆 𝑢 ) ) )
91 90 cbvfo ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑣 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) ↔ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐴 ( 𝑢 𝑆 ( 𝐹 ‘ 𝑣 ) ∨ 𝑢 = ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑣 ) 𝑆 𝑢 ) ) )
92 breq2 ⊢ ( ( 𝐹 ‘ 𝑣 ) = 𝑓 → ( 𝑢 𝑆 ( 𝐹 ‘ 𝑣 ) ↔ 𝑢 𝑆 𝑓 ) )
93 eqeq2 ⊢ ( ( 𝐹 ‘ 𝑣 ) = 𝑓 → ( 𝑢 = ( 𝐹 ‘ 𝑣 ) ↔ 𝑢 = 𝑓 ) )
94 breq1 ⊢ ( ( 𝐹 ‘ 𝑣 ) = 𝑓 → ( ( 𝐹 ‘ 𝑣 ) 𝑆 𝑢 ↔ 𝑓 𝑆 𝑢 ) )
95 92 93 94 3orbi123d ⊢ ( ( 𝐹 ‘ 𝑣 ) = 𝑓 → ( ( 𝑢 𝑆 ( 𝐹 ‘ 𝑣 ) ∨ 𝑢 = ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑣 ) 𝑆 𝑢 ) ↔ ( 𝑢 𝑆 𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓 𝑆 𝑢 ) ) )
96 95 cbvfo ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ∀ 𝑣 ∈ 𝐴 ( 𝑢 𝑆 ( 𝐹 ‘ 𝑣 ) ∨ 𝑢 = ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑣 ) 𝑆 𝑢 ) ↔ ∀ 𝑓 ∈ 𝐵 ( 𝑢 𝑆 𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓 𝑆 𝑢 ) ) )
97 96 ralbidv ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐴 ( 𝑢 𝑆 ( 𝐹 ‘ 𝑣 ) ∨ 𝑢 = ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑣 ) 𝑆 𝑢 ) ↔ ∀ 𝑢 ∈ 𝐵 ∀ 𝑓 ∈ 𝐵 ( 𝑢 𝑆 𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓 𝑆 𝑢 ) ) )
98 91 97 bitrd ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑣 ) ∨ ( 𝐹 ‘ 𝑣 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) ↔ ∀ 𝑢 ∈ 𝐵 ∀ 𝑓 ∈ 𝐵 ( 𝑢 𝑆 𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓 𝑆 𝑢 ) ) )
99 85 98 sylan9bb ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑤 𝑅 𝑣 ∨ 𝑤 = 𝑣 ∨ 𝑣 𝑅 𝑤 ) ↔ ∀ 𝑢 ∈ 𝐵 ∀ 𝑓 ∈ 𝐵 ( 𝑢 𝑆 𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓 𝑆 𝑢 ) ) )
100 74 99 sylbi ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑤 𝑅 𝑣 ∨ 𝑤 = 𝑣 ∨ 𝑣 𝑅 𝑤 ) ↔ ∀ 𝑢 ∈ 𝐵 ∀ 𝑓 ∈ 𝐵 ( 𝑢 𝑆 𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓 𝑆 𝑢 ) ) )
101 100 biimprd ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑓 ∈ 𝐵 ( 𝑢 𝑆 𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓 𝑆 𝑢 ) → ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑤 𝑅 𝑣 ∨ 𝑤 = 𝑣 ∨ 𝑣 𝑅 𝑤 ) ) )
102 73 101 anim12d ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( ( 𝑆 Fr 𝐵 ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑓 ∈ 𝐵 ( 𝑢 𝑆 𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓 𝑆 𝑢 ) ) → ( 𝑅 Fr 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑤 𝑅 𝑣 ∨ 𝑤 = 𝑣 ∨ 𝑣 𝑅 𝑤 ) ) ) )
103 dfwe2 ⊢ ( 𝑆 We 𝐵 ↔ ( 𝑆 Fr 𝐵 ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑓 ∈ 𝐵 ( 𝑢 𝑆 𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓 𝑆 𝑢 ) ) )
104 dfwe2 ⊢ ( 𝑅 We 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑤 𝑅 𝑣 ∨ 𝑤 = 𝑣 ∨ 𝑣 𝑅 𝑤 ) ) )
105 102 103 104 3imtr4g ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( 𝑆 We 𝐵 → 𝑅 We 𝐴 ) )