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 𝐴 ) )