Theorem f1oweALT 7975

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

Hypothesis

Ref	Expression
f1oweALT.1	⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)}

Assertion

Ref	Expression
f1oweALT	⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴))

Distinct variable groups:   𝑥,𝑦,𝑆   𝑥,𝐹,𝑦

Allowed substitution hints:   𝐴(𝑥, 𝑦)   𝐵(𝑥, 𝑦)   𝑅(𝑥, 𝑦)

Proof of Theorem f1oweALT

Dummy variables 𝑧 𝑤 𝑣 𝑢 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1ofo 6832	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)
2		df-fo 6546	. . . . 5 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
3		freq2 5631	. . . . . . 7 ⊢ (ran 𝐹 = 𝐵 → (𝑆 Fr ran 𝐹 ↔ 𝑆 Fr 𝐵))
4	3	biimprd 251	. . . . . 6 ⊢ (ran 𝐹 = 𝐵 → (𝑆 Fr 𝐵 → 𝑆 Fr ran 𝐹))
5		df-fn 6543	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fr 5616	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑆 Fr ran 𝐹 ↔ ∀𝑤((𝑤 ⊆ ran 𝐹 ∧ 𝑤 ≠ ∅) → ∃𝑢 ∈ 𝑤 ∀𝑓 ∈ 𝑤 ¬ 𝑓𝑆𝑢))
7		vex 3461	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑧 ∈ V
8	7	funimaex 6627	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fun 𝐹 → (𝐹 “ 𝑧) ∈ V)
9		n0 4307	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ≠ ∅ ↔ ∃𝑤 𝑤 ∈ 𝑧)
10		funfvima2 7236	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) → (𝑤 ∈ 𝑧 → (𝐹‘𝑤) ∈ (𝐹 “ 𝑧)))
11		ne0i 4294	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹‘𝑤) ∈ (𝐹 “ 𝑧) → (𝐹 “ 𝑧) ≠ ∅)
12	10, 11	syl6 36	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) → (𝑤 ∈ 𝑧 → (𝐹 “ 𝑧) ≠ ∅))
13	12	exlimdv 1966	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) → (∃𝑤 𝑤 ∈ 𝑧 → (𝐹 “ 𝑧) ≠ ∅))
14	9, 13	biimtrid 245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) → (𝑧 ≠ ∅ → (𝐹 “ 𝑧) ≠ ∅))
15	14	imp 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) ∧ 𝑧 ≠ ∅) → (𝐹 “ 𝑧) ≠ ∅)
16		imassrn 6075	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 “ 𝑧) ⊆ ran 𝐹
17	15, 16	jctil 529	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) ∧ 𝑧 ≠ ∅) → ((𝐹 “ 𝑧) ⊆ ran 𝐹 ∧ (𝐹 “ 𝑧) ≠ ∅))
18		sseq1 3963	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (𝐹 “ 𝑧) → (𝑤 ⊆ ran 𝐹 ↔ (𝐹 “ 𝑧) ⊆ ran 𝐹))
19		neeq1 3022	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (𝐹 “ 𝑧) → (𝑤 ≠ ∅ ↔ (𝐹 “ 𝑧) ≠ ∅))
20	18, 19	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝐹 “ 𝑧) → ((𝑤 ⊆ ran 𝐹 ∧ 𝑤 ≠ ∅) ↔ ((𝐹 “ 𝑧) ⊆ ran 𝐹 ∧ (𝐹 “ 𝑧) ≠ ∅)))
21		raleq 3322	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (𝐹 “ 𝑧) → (∀𝑓 ∈ 𝑤 ¬ 𝑓𝑆𝑢 ↔ ∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢))
22	21	rexeqbi1dv 3336	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝐹 “ 𝑧) → (∃𝑢 ∈ 𝑤 ∀𝑓 ∈ 𝑤 ¬ 𝑓𝑆𝑢 ↔ ∃𝑢 ∈ (𝐹 “ 𝑧)∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢))
23	20, 22	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (𝐹 “ 𝑧) → (((𝑤 ⊆ ran 𝐹 ∧ 𝑤 ≠ ∅) → ∃𝑢 ∈ 𝑤 ∀𝑓 ∈ 𝑤 ¬ 𝑓𝑆𝑢) ↔ (((𝐹 “ 𝑧) ⊆ ran 𝐹 ∧ (𝐹 “ 𝑧) ≠ ∅) → ∃𝑢 ∈ (𝐹 “ 𝑧)∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢)))
24	23	spcgv 3557	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 “ 𝑧) ∈ V → (∀𝑤((𝑤 ⊆ ran 𝐹 ∧ 𝑤 ≠ ∅) → ∃𝑢 ∈ 𝑤 ∀𝑓 ∈ 𝑤 ¬ 𝑓𝑆𝑢) → (((𝐹 “ 𝑧) ⊆ ran 𝐹 ∧ (𝐹 “ 𝑧) ≠ ∅) → ∃𝑢 ∈ (𝐹 “ 𝑧)∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢)))
25	17, 24	syl7 75	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 “ 𝑧) ∈ V → (∀𝑤((𝑤 ⊆ ran 𝐹 ∧ 𝑤 ≠ ∅) → ∃𝑢 ∈ 𝑤 ∀𝑓 ∈ 𝑤 ¬ 𝑓𝑆𝑢) → (((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) ∧ 𝑧 ≠ ∅) → ∃𝑢 ∈ (𝐹 “ 𝑧)∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢)))
26	8, 25	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Fun 𝐹 → (∀𝑤((𝑤 ⊆ ran 𝐹 ∧ 𝑤 ≠ ∅) → ∃𝑢 ∈ 𝑤 ∀𝑓 ∈ 𝑤 ¬ 𝑓𝑆𝑢) → (((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) ∧ 𝑧 ≠ ∅) → ∃𝑢 ∈ (𝐹 “ 𝑧)∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢)))
27	6, 26	biimtrid 245	. . . . . . . . . . . . . . . . . . 19 ⊢ (Fun 𝐹 → (𝑆 Fr ran 𝐹 → (((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) ∧ 𝑧 ≠ ∅) → ∃𝑢 ∈ (𝐹 “ 𝑧)∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢)))
28	27	com23 87	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝐹 → (((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) ∧ 𝑧 ≠ ∅) → (𝑆 Fr ran 𝐹 → ∃𝑢 ∈ (𝐹 “ 𝑧)∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢)))
29	28	expd 421	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝐹 → ((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) → (𝑧 ≠ ∅ → (𝑆 Fr ran 𝐹 → ∃𝑢 ∈ (𝐹 “ 𝑧)∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢))))
30	29	anabsi5 682	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) → (𝑧 ≠ ∅ → (𝑆 Fr ran 𝐹 → ∃𝑢 ∈ (𝐹 “ 𝑧)∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢)))
31	30	impd 416	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) → ((𝑧 ≠ ∅ ∧ 𝑆 Fr ran 𝐹) → ∃𝑢 ∈ (𝐹 “ 𝑧)∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢))
32		fores 6806	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) → (𝐹 ↾ 𝑧):𝑧–onto→(𝐹 “ 𝑧))
33		vex 3461	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑣 ∈ V
34		vex 3461	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑤 ∈ V
35		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
36	35	breq1d 5121	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥)𝑆(𝐹‘𝑦) ↔ (𝐹‘𝑣)𝑆(𝐹‘𝑦)))
37		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
38	37	breq2d 5123	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑤 → ((𝐹‘𝑣)𝑆(𝐹‘𝑦) ↔ (𝐹‘𝑣)𝑆(𝐹‘𝑤)))
39		f1oweALT.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)}
40	33, 34, 36, 38, 39	brab 5530	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣𝑅𝑤 ↔ (𝐹‘𝑣)𝑆(𝐹‘𝑤))
41		fvres 6904	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ 𝑧 → ((𝐹 ↾ 𝑧)‘𝑣) = (𝐹‘𝑣))
42		fvres 6904	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ 𝑧 → ((𝐹 ↾ 𝑧)‘𝑤) = (𝐹‘𝑤))
43	41, 42	breqan12rd 5128	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧) → (((𝐹 ↾ 𝑧)‘𝑣)𝑆((𝐹 ↾ 𝑧)‘𝑤) ↔ (𝐹‘𝑣)𝑆(𝐹‘𝑤)))
44	40, 43	bitr4id 293	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧) → (𝑣𝑅𝑤 ↔ ((𝐹 ↾ 𝑧)‘𝑣)𝑆((𝐹 ↾ 𝑧)‘𝑤)))
45	44	notbid 321	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧) → (¬ 𝑣𝑅𝑤 ↔ ¬ ((𝐹 ↾ 𝑧)‘𝑣)𝑆((𝐹 ↾ 𝑧)‘𝑤)))
46	45	ralbidva 3188	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ 𝑧 → (∀𝑣 ∈ 𝑧 ¬ 𝑣𝑅𝑤 ↔ ∀𝑣 ∈ 𝑧 ¬ ((𝐹 ↾ 𝑧)‘𝑣)𝑆((𝐹 ↾ 𝑧)‘𝑤)))
47	46	rexbiia 3112	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑤 ∈ 𝑧 ∀𝑣 ∈ 𝑧 ¬ 𝑣𝑅𝑤 ↔ ∃𝑤 ∈ 𝑧 ∀𝑣 ∈ 𝑧 ¬ ((𝐹 ↾ 𝑧)‘𝑣)𝑆((𝐹 ↾ 𝑧)‘𝑤))
48		breq1 5114	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ↾ 𝑧)‘𝑣) = 𝑓 → (((𝐹 ↾ 𝑧)‘𝑣)𝑆((𝐹 ↾ 𝑧)‘𝑤) ↔ 𝑓𝑆((𝐹 ↾ 𝑧)‘𝑤)))
49	48	notbid 321	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ↾ 𝑧)‘𝑣) = 𝑓 → (¬ ((𝐹 ↾ 𝑧)‘𝑣)𝑆((𝐹 ↾ 𝑧)‘𝑤) ↔ ¬ 𝑓𝑆((𝐹 ↾ 𝑧)‘𝑤)))
50	49	cbvfo 7296	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ↾ 𝑧):𝑧–onto→(𝐹 “ 𝑧) → (∀𝑣 ∈ 𝑧 ¬ ((𝐹 ↾ 𝑧)‘𝑣)𝑆((𝐹 ↾ 𝑧)‘𝑤) ↔ ∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆((𝐹 ↾ 𝑧)‘𝑤)))
51	50	rexbidv 3191	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ↾ 𝑧):𝑧–onto→(𝐹 “ 𝑧) → (∃𝑤 ∈ 𝑧 ∀𝑣 ∈ 𝑧 ¬ ((𝐹 ↾ 𝑧)‘𝑣)𝑆((𝐹 ↾ 𝑧)‘𝑤) ↔ ∃𝑤 ∈ 𝑧 ∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆((𝐹 ↾ 𝑧)‘𝑤)))
52		breq2 5115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ↾ 𝑧)‘𝑤) = 𝑢 → (𝑓𝑆((𝐹 ↾ 𝑧)‘𝑤) ↔ 𝑓𝑆𝑢))
53	52	notbid 321	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ↾ 𝑧)‘𝑤) = 𝑢 → (¬ 𝑓𝑆((𝐹 ↾ 𝑧)‘𝑤) ↔ ¬ 𝑓𝑆𝑢))
54	53	ralbidv 3190	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ↾ 𝑧)‘𝑤) = 𝑢 → (∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆((𝐹 ↾ 𝑧)‘𝑤) ↔ ∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢))
55	54	cbvexfo 7297	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ↾ 𝑧):𝑧–onto→(𝐹 “ 𝑧) → (∃𝑤 ∈ 𝑧 ∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆((𝐹 ↾ 𝑧)‘𝑤) ↔ ∃𝑢 ∈ (𝐹 “ 𝑧)∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢))
56	51, 55	bitrd 282	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ↾ 𝑧):𝑧–onto→(𝐹 “ 𝑧) → (∃𝑤 ∈ 𝑧 ∀𝑣 ∈ 𝑧 ¬ ((𝐹 ↾ 𝑧)‘𝑣)𝑆((𝐹 ↾ 𝑧)‘𝑤) ↔ ∃𝑢 ∈ (𝐹 “ 𝑧)∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢))
57	47, 56	bitrid 286	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ↾ 𝑧):𝑧–onto→(𝐹 “ 𝑧) → (∃𝑤 ∈ 𝑧 ∀𝑣 ∈ 𝑧 ¬ 𝑣𝑅𝑤 ↔ ∃𝑢 ∈ (𝐹 “ 𝑧)∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢))
58	32, 57	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) → (∃𝑤 ∈ 𝑧 ∀𝑣 ∈ 𝑧 ¬ 𝑣𝑅𝑤 ↔ ∃𝑢 ∈ (𝐹 “ 𝑧)∀𝑓 ∈ (𝐹 “ 𝑧) ¬ 𝑓𝑆𝑢))
59	31, 58	sylibrd 262	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐹 ∧ 𝑧 ⊆ dom 𝐹) → ((𝑧 ≠ ∅ ∧ 𝑆 Fr ran 𝐹) → ∃𝑤 ∈ 𝑧 ∀𝑣 ∈ 𝑧 ¬ 𝑣𝑅𝑤))
60	59	exp4b 436	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 → (𝑧 ⊆ dom 𝐹 → (𝑧 ≠ ∅ → (𝑆 Fr ran 𝐹 → ∃𝑤 ∈ 𝑧 ∀𝑣 ∈ 𝑧 ¬ 𝑣𝑅𝑤))))
61	60	com34 92	. . . . . . . . . . . 12 ⊢ (Fun 𝐹 → (𝑧 ⊆ dom 𝐹 → (𝑆 Fr ran 𝐹 → (𝑧 ≠ ∅ → ∃𝑤 ∈ 𝑧 ∀𝑣 ∈ 𝑧 ¬ 𝑣𝑅𝑤))))
62	61	com23 87	. . . . . . . . . . 11 ⊢ (Fun 𝐹 → (𝑆 Fr ran 𝐹 → (𝑧 ⊆ dom 𝐹 → (𝑧 ≠ ∅ → ∃𝑤 ∈ 𝑧 ∀𝑣 ∈ 𝑧 ¬ 𝑣𝑅𝑤))))
63	62	imp4a 428	. . . . . . . . . 10 ⊢ (Fun 𝐹 → (𝑆 Fr ran 𝐹 → ((𝑧 ⊆ dom 𝐹 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 ∀𝑣 ∈ 𝑧 ¬ 𝑣𝑅𝑤)))
64	63	alrimdv 1962	. . . . . . . . 9 ⊢ (Fun 𝐹 → (𝑆 Fr ran 𝐹 → ∀𝑧((𝑧 ⊆ dom 𝐹 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 ∀𝑣 ∈ 𝑧 ¬ 𝑣𝑅𝑤)))
65		df-fr 5616	. . . . . . . . 9 ⊢ (𝑅 Fr dom 𝐹 ↔ ∀𝑧((𝑧 ⊆ dom 𝐹 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 ∀𝑣 ∈ 𝑧 ¬ 𝑣𝑅𝑤))
66	64, 65	imbitrrdi 255	. . . . . . . 8 ⊢ (Fun 𝐹 → (𝑆 Fr ran 𝐹 → 𝑅 Fr dom 𝐹))
67		freq2 5631	. . . . . . . . 9 ⊢ (dom 𝐹 = 𝐴 → (𝑅 Fr dom 𝐹 ↔ 𝑅 Fr 𝐴))
68	67	biimpd 232	. . . . . . . 8 ⊢ (dom 𝐹 = 𝐴 → (𝑅 Fr dom 𝐹 → 𝑅 Fr 𝐴))
69	66, 68	sylan9 517	. . . . . . 7 ⊢ ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) → (𝑆 Fr ran 𝐹 → 𝑅 Fr 𝐴))
70	5, 69	sylbi 220	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑆 Fr ran 𝐹 → 𝑅 Fr 𝐴))
71	4, 70	sylan9r 518	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))
72	2, 71	sylbi 220	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))
73	1, 72	syl 18	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))
74		df-f1o 6547	. . . . 5 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
75		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
76	75	breq1d 5121	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥)𝑆(𝐹‘𝑦) ↔ (𝐹‘𝑤)𝑆(𝐹‘𝑦)))
77		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑣 → (𝐹‘𝑦) = (𝐹‘𝑣))
78	77	breq2d 5123	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → ((𝐹‘𝑤)𝑆(𝐹‘𝑦) ↔ (𝐹‘𝑤)𝑆(𝐹‘𝑣)))
79	34, 33, 76, 78, 39	brab 5530	. . . . . . . . 9 ⊢ (𝑤𝑅𝑣 ↔ (𝐹‘𝑤)𝑆(𝐹‘𝑣))
80	79	a1i 11	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑤𝑅𝑣 ↔ (𝐹‘𝑤)𝑆(𝐹‘𝑣)))
81		f1fveq 7265	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → ((𝐹‘𝑤) = (𝐹‘𝑣) ↔ 𝑤 = 𝑣))
82	81	bicomd 226	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑤 = 𝑣 ↔ (𝐹‘𝑤) = (𝐹‘𝑣)))
83	40	a1i 11	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑣𝑅𝑤 ↔ (𝐹‘𝑣)𝑆(𝐹‘𝑤)))
84	80, 82, 83	3orbi123d 1463	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → ((𝑤𝑅𝑣 ∨ 𝑤 = 𝑣 ∨ 𝑣𝑅𝑤) ↔ ((𝐹‘𝑤)𝑆(𝐹‘𝑣) ∨ (𝐹‘𝑤) = (𝐹‘𝑣) ∨ (𝐹‘𝑣)𝑆(𝐹‘𝑤))))
85	84	2ralbidva 3229	. . . . . 6 ⊢ (𝐹:𝐴–1-1→𝐵 → (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑤𝑅𝑣 ∨ 𝑤 = 𝑣 ∨ 𝑣𝑅𝑤) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((𝐹‘𝑤)𝑆(𝐹‘𝑣) ∨ (𝐹‘𝑤) = (𝐹‘𝑣) ∨ (𝐹‘𝑣)𝑆(𝐹‘𝑤))))
86		breq1 5114	. . . . . . . . . 10 ⊢ ((𝐹‘𝑤) = 𝑢 → ((𝐹‘𝑤)𝑆(𝐹‘𝑣) ↔ 𝑢𝑆(𝐹‘𝑣)))
87		eqeq1 2769	. . . . . . . . . 10 ⊢ ((𝐹‘𝑤) = 𝑢 → ((𝐹‘𝑤) = (𝐹‘𝑣) ↔ 𝑢 = (𝐹‘𝑣)))
88		breq2 5115	. . . . . . . . . 10 ⊢ ((𝐹‘𝑤) = 𝑢 → ((𝐹‘𝑣)𝑆(𝐹‘𝑤) ↔ (𝐹‘𝑣)𝑆𝑢))
89	86, 87, 88	3orbi123d 1463	. . . . . . . . 9 ⊢ ((𝐹‘𝑤) = 𝑢 → (((𝐹‘𝑤)𝑆(𝐹‘𝑣) ∨ (𝐹‘𝑤) = (𝐹‘𝑣) ∨ (𝐹‘𝑣)𝑆(𝐹‘𝑤)) ↔ (𝑢𝑆(𝐹‘𝑣) ∨ 𝑢 = (𝐹‘𝑣) ∨ (𝐹‘𝑣)𝑆𝑢)))
90	89	ralbidv 3190	. . . . . . . 8 ⊢ ((𝐹‘𝑤) = 𝑢 → (∀𝑣 ∈ 𝐴 ((𝐹‘𝑤)𝑆(𝐹‘𝑣) ∨ (𝐹‘𝑤) = (𝐹‘𝑣) ∨ (𝐹‘𝑣)𝑆(𝐹‘𝑤)) ↔ ∀𝑣 ∈ 𝐴 (𝑢𝑆(𝐹‘𝑣) ∨ 𝑢 = (𝐹‘𝑣) ∨ (𝐹‘𝑣)𝑆𝑢)))
91	90	cbvfo 7296	. . . . . . 7 ⊢ (𝐹:𝐴–onto→𝐵 → (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((𝐹‘𝑤)𝑆(𝐹‘𝑣) ∨ (𝐹‘𝑤) = (𝐹‘𝑣) ∨ (𝐹‘𝑣)𝑆(𝐹‘𝑤)) ↔ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐴 (𝑢𝑆(𝐹‘𝑣) ∨ 𝑢 = (𝐹‘𝑣) ∨ (𝐹‘𝑣)𝑆𝑢)))
92		breq2 5115	. . . . . . . . . 10 ⊢ ((𝐹‘𝑣) = 𝑓 → (𝑢𝑆(𝐹‘𝑣) ↔ 𝑢𝑆𝑓))
93		eqeq2 2777	. . . . . . . . . 10 ⊢ ((𝐹‘𝑣) = 𝑓 → (𝑢 = (𝐹‘𝑣) ↔ 𝑢 = 𝑓))
94		breq1 5114	. . . . . . . . . 10 ⊢ ((𝐹‘𝑣) = 𝑓 → ((𝐹‘𝑣)𝑆𝑢 ↔ 𝑓𝑆𝑢))
95	92, 93, 94	3orbi123d 1463	. . . . . . . . 9 ⊢ ((𝐹‘𝑣) = 𝑓 → ((𝑢𝑆(𝐹‘𝑣) ∨ 𝑢 = (𝐹‘𝑣) ∨ (𝐹‘𝑣)𝑆𝑢) ↔ (𝑢𝑆𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓𝑆𝑢)))
96	95	cbvfo 7296	. . . . . . . 8 ⊢ (𝐹:𝐴–onto→𝐵 → (∀𝑣 ∈ 𝐴 (𝑢𝑆(𝐹‘𝑣) ∨ 𝑢 = (𝐹‘𝑣) ∨ (𝐹‘𝑣)𝑆𝑢) ↔ ∀𝑓 ∈ 𝐵 (𝑢𝑆𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓𝑆𝑢)))
97	96	ralbidv 3190	. . . . . . 7 ⊢ (𝐹:𝐴–onto→𝐵 → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐴 (𝑢𝑆(𝐹‘𝑣) ∨ 𝑢 = (𝐹‘𝑣) ∨ (𝐹‘𝑣)𝑆𝑢) ↔ ∀𝑢 ∈ 𝐵 ∀𝑓 ∈ 𝐵 (𝑢𝑆𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓𝑆𝑢)))
98	91, 97	bitrd 282	. . . . . 6 ⊢ (𝐹:𝐴–onto→𝐵 → (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((𝐹‘𝑤)𝑆(𝐹‘𝑣) ∨ (𝐹‘𝑤) = (𝐹‘𝑣) ∨ (𝐹‘𝑣)𝑆(𝐹‘𝑤)) ↔ ∀𝑢 ∈ 𝐵 ∀𝑓 ∈ 𝐵 (𝑢𝑆𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓𝑆𝑢)))
99	85, 98	sylan9bb 519	. . . . 5 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) → (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑤𝑅𝑣 ∨ 𝑤 = 𝑣 ∨ 𝑣𝑅𝑤) ↔ ∀𝑢 ∈ 𝐵 ∀𝑓 ∈ 𝐵 (𝑢𝑆𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓𝑆𝑢)))
100	74, 99	sylbi 220	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑤𝑅𝑣 ∨ 𝑤 = 𝑣 ∨ 𝑣𝑅𝑤) ↔ ∀𝑢 ∈ 𝐵 ∀𝑓 ∈ 𝐵 (𝑢𝑆𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓𝑆𝑢)))
101	100	biimprd 251	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (∀𝑢 ∈ 𝐵 ∀𝑓 ∈ 𝐵 (𝑢𝑆𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓𝑆𝑢) → ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑤𝑅𝑣 ∨ 𝑤 = 𝑣 ∨ 𝑣𝑅𝑤)))
102	73, 101	anim12d 621	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝑆 Fr 𝐵 ∧ ∀𝑢 ∈ 𝐵 ∀𝑓 ∈ 𝐵 (𝑢𝑆𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓𝑆𝑢)) → (𝑅 Fr 𝐴 ∧ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑤𝑅𝑣 ∨ 𝑤 = 𝑣 ∨ 𝑣𝑅𝑤))))
103		dfwe2 7779	. 2 ⊢ (𝑆 We 𝐵 ↔ (𝑆 Fr 𝐵 ∧ ∀𝑢 ∈ 𝐵 ∀𝑓 ∈ 𝐵 (𝑢𝑆𝑓 ∨ 𝑢 = 𝑓 ∨ 𝑓𝑆𝑢)))
104		dfwe2 7779	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑤𝑅𝑣 ∨ 𝑤 = 𝑣 ∨ 𝑣𝑅𝑤)))
105	102, 103, 104	3imtr4g 299	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ w3o 1102  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2146   ≠ wne 2960  ∀wral 3081  ∃wrex 3091  Vcvv 3457   ⊆ wss 3906  ∅c0 4286   class class class wbr 5111  {copab 5175   Fr wfr 5613   We wwe 5615  dom cdm 5663  ran crn 5664   ↾ cres 5665   “ cima 5666  Fun wfun 6534   Fn wfn 6535  –1-1→wf1 6537  –onto→wfo 6538  –1-1-onto→wf1o 6539  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548

This theorem is used by: (None)