f1oweALT

Description: Alternate proof of one direction 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	$⊢ R = \{⟨x, y⟩ \| F (x) S F (y)\}$
	Assertion	f1oweALT	$⊢ F : A \underset{1-1 onto}{⟶} B \to (S We B \to R We A)$

Proof

Step	Hyp	Ref	Expression
1		f1oweALT.1	$⊢ R = \{⟨x, y⟩ \| F (x) S F (y)\}$
2		f1ofo	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{onto}{⟶} B$
3		df-fo	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F Fn A \land ran F = B)$
4		freq2	$⊢ ran F = B \to (S Fr ran F \leftrightarrow S Fr B)$
5	4	biimprd	$⊢ ran F = B \to (S Fr B \to S Fr ran F)$
6		df-fn	$⊢ F Fn A \leftrightarrow (Fun F \land dom F = A)$
7		df-fr	$⊢ S Fr ran F \leftrightarrow \forall w ((w \subseteq ran F \land w \neq \emptyset) \to \exists u \in w \forall f \in w \neg f S u)$
8		vex	$⊢ z \in V$
9	8	funimaex	$⊢ Fun F \to F [z] \in V$
10		n0	$⊢ z \neq \emptyset \leftrightarrow \exists w w \in z$
11		funfvima2	$⊢ (Fun F \land z \subseteq dom F) \to (w \in z \to F (w) \in F [z])$
12		ne0i	$⊢ F (w) \in F [z] \to F [z] \neq \emptyset$
13	11 12	syl6	$⊢ (Fun F \land z \subseteq dom F) \to (w \in z \to F [z] \neq \emptyset)$
14	13	exlimdv	$⊢ (Fun F \land z \subseteq dom F) \to (\exists w w \in z \to F [z] \neq \emptyset)$
15	10 14	biimtrid	$⊢ (Fun F \land z \subseteq dom F) \to (z \neq \emptyset \to F [z] \neq \emptyset)$
16	15	imp	$⊢ ((Fun F \land z \subseteq dom F) \land z \neq \emptyset) \to F [z] \neq \emptyset$
17		imassrn	$⊢ F [z] \subseteq ran F$
18	16 17	jctil	$⊢ ((Fun F \land z \subseteq dom F) \land z \neq \emptyset) \to (F [z] \subseteq ran F \land F [z] \neq \emptyset)$
19		sseq1	$⊢ w = F [z] \to (w \subseteq ran F \leftrightarrow F [z] \subseteq ran F)$
20		neeq1	$⊢ w = F [z] \to (w \neq \emptyset \leftrightarrow F [z] \neq \emptyset)$
21	19 20	anbi12d	$⊢ w = F [z] \to ((w \subseteq ran F \land w \neq \emptyset) \leftrightarrow (F [z] \subseteq ran F \land F [z] \neq \emptyset))$
22		raleq	$⊢ w = F [z] \to (\forall f \in w \neg f S u \leftrightarrow \forall f \in F [z] \neg f S u)$
23	22	rexeqbi1dv	$⊢ w = F [z] \to (\exists u \in w \forall f \in w \neg f S u \leftrightarrow \exists u \in F [z] \forall f \in F [z] \neg f S u)$
24	21 23	imbi12d	$⊢ w = F [z] \to (((w \subseteq ran F \land w \neq \emptyset) \to \exists u \in w \forall f \in w \neg f S u) \leftrightarrow ((F [z] \subseteq ran F \land F [z] \neq \emptyset) \to \exists u \in F [z] \forall f \in F [z] \neg f S u))$
25	24	spcgv	$⊢ F [z] \in V \to (\forall w ((w \subseteq ran F \land w \neq \emptyset) \to \exists u \in w \forall f \in w \neg f S u) \to ((F [z] \subseteq ran F \land F [z] \neq \emptyset) \to \exists u \in F [z] \forall f \in F [z] \neg f S u))$
26	18 25	syl7	$⊢ F [z] \in V \to (\forall w ((w \subseteq ran F \land w \neq \emptyset) \to \exists u \in w \forall f \in w \neg f S u) \to (((Fun F \land z \subseteq dom F) \land z \neq \emptyset) \to \exists u \in F [z] \forall f \in F [z] \neg f S u))$
27	9 26	syl	$⊢ Fun F \to (\forall w ((w \subseteq ran F \land w \neq \emptyset) \to \exists u \in w \forall f \in w \neg f S u) \to (((Fun F \land z \subseteq dom F) \land z \neq \emptyset) \to \exists u \in F [z] \forall f \in F [z] \neg f S u))$
28	7 27	biimtrid	$⊢ Fun F \to (S Fr ran F \to (((Fun F \land z \subseteq dom F) \land z \neq \emptyset) \to \exists u \in F [z] \forall f \in F [z] \neg f S u))$
29	28	com23	$⊢ Fun F \to (((Fun F \land z \subseteq dom F) \land z \neq \emptyset) \to (S Fr ran F \to \exists u \in F [z] \forall f \in F [z] \neg f S u))$
30	29	expd	$⊢ Fun F \to ((Fun F \land z \subseteq dom F) \to (z \neq \emptyset \to (S Fr ran F \to \exists u \in F [z] \forall f \in F [z] \neg f S u)))$
31	30	anabsi5	$⊢ (Fun F \land z \subseteq dom F) \to (z \neq \emptyset \to (S Fr ran F \to \exists u \in F [z] \forall f \in F [z] \neg f S u))$
32	31	impd	$⊢ (Fun F \land z \subseteq dom F) \to ((z \neq \emptyset \land S Fr ran F) \to \exists u \in F [z] \forall f \in F [z] \neg f S u)$
33		fores	$⊢ (Fun F \land z \subseteq dom F) \to ({F ↾}_{z}) : z \underset{onto}{⟶} F [z]$
34		vex	$⊢ v \in V$
35		vex	$⊢ w \in V$
36		fveq2	$⊢ x = v \to F (x) = F (v)$
37	36	breq1d	$⊢ x = v \to (F (x) S F (y) \leftrightarrow F (v) S F (y))$
38		fveq2	$⊢ y = w \to F (y) = F (w)$
39	38	breq2d	$⊢ y = w \to (F (v) S F (y) \leftrightarrow F (v) S F (w))$
40	34 35 37 39 1	brab	$⊢ v R w \leftrightarrow F (v) S F (w)$
41		fvres	$⊢ v \in z \to ({F ↾}_{z}) (v) = F (v)$
42		fvres	$⊢ w \in z \to ({F ↾}_{z}) (w) = F (w)$
43	41 42	breqan12rd	$⊢ (w \in z \land v \in z) \to (({F ↾}_{z}) (v) S ({F ↾}_{z}) (w) \leftrightarrow F (v) S F (w))$
44	40 43	bitr4id	$⊢ (w \in z \land v \in z) \to (v R w \leftrightarrow ({F ↾}_{z}) (v) S ({F ↾}_{z}) (w))$
45	44	notbid	$⊢ (w \in z \land v \in z) \to (\neg v R w \leftrightarrow \neg ({F ↾}_{z}) (v) S ({F ↾}_{z}) (w))$
46	45	ralbidva	$⊢ w \in z \to (\forall v \in z \neg v R w \leftrightarrow \forall v \in z \neg ({F ↾}_{z}) (v) S ({F ↾}_{z}) (w))$
47	46	rexbiia	$⊢ \exists w \in z \forall v \in z \neg v R w \leftrightarrow \exists w \in z \forall v \in z \neg ({F ↾}_{z}) (v) S ({F ↾}_{z}) (w)$
48		breq1	$⊢ ({F ↾}_{z}) (v) = f \to (({F ↾}_{z}) (v) S ({F ↾}_{z}) (w) \leftrightarrow f S ({F ↾}_{z}) (w))$
49	48	notbid	$⊢ ({F ↾}_{z}) (v) = f \to (\neg ({F ↾}_{z}) (v) S ({F ↾}_{z}) (w) \leftrightarrow \neg f S ({F ↾}_{z}) (w))$
50	49	cbvfo	$⊢ ({F ↾}_{z}) : z \underset{onto}{⟶} F [z] \to (\forall v \in z \neg ({F ↾}_{z}) (v) S ({F ↾}_{z}) (w) \leftrightarrow \forall f \in F [z] \neg f S ({F ↾}_{z}) (w))$
51	50	rexbidv	$⊢ ({F ↾}_{z}) : z \underset{onto}{⟶} F [z] \to (\exists w \in z \forall v \in z \neg ({F ↾}_{z}) (v) S ({F ↾}_{z}) (w) \leftrightarrow \exists w \in z \forall f \in F [z] \neg f S ({F ↾}_{z}) (w))$
52		breq2	$⊢ ({F ↾}_{z}) (w) = u \to (f S ({F ↾}_{z}) (w) \leftrightarrow f S u)$
53	52	notbid	$⊢ ({F ↾}_{z}) (w) = u \to (\neg f S ({F ↾}_{z}) (w) \leftrightarrow \neg f S u)$
54	53	ralbidv	$⊢ ({F ↾}_{z}) (w) = u \to (\forall f \in F [z] \neg f S ({F ↾}_{z}) (w) \leftrightarrow \forall f \in F [z] \neg f S u)$
55	54	cbvexfo	$⊢ ({F ↾}_{z}) : z \underset{onto}{⟶} F [z] \to (\exists w \in z \forall f \in F [z] \neg f S ({F ↾}_{z}) (w) \leftrightarrow \exists u \in F [z] \forall f \in F [z] \neg f S u)$
56	51 55	bitrd	$⊢ ({F ↾}_{z}) : z \underset{onto}{⟶} F [z] \to (\exists w \in z \forall v \in z \neg ({F ↾}_{z}) (v) S ({F ↾}_{z}) (w) \leftrightarrow \exists u \in F [z] \forall f \in F [z] \neg f S u)$
57	47 56	bitrid	$⊢ ({F ↾}_{z}) : z \underset{onto}{⟶} F [z] \to (\exists w \in z \forall v \in z \neg v R w \leftrightarrow \exists u \in F [z] \forall f \in F [z] \neg f S u)$
58	33 57	syl	$⊢ (Fun F \land z \subseteq dom F) \to (\exists w \in z \forall v \in z \neg v R w \leftrightarrow \exists u \in F [z] \forall f \in F [z] \neg f S u)$
59	32 58	sylibrd	$⊢ (Fun F \land z \subseteq dom F) \to ((z \neq \emptyset \land S Fr ran F) \to \exists w \in z \forall v \in z \neg v R w)$
60	59	exp4b	$⊢ Fun F \to (z \subseteq dom F \to (z \neq \emptyset \to (S Fr ran F \to \exists w \in z \forall v \in z \neg v R w)))$
61	60	com34	$⊢ Fun F \to (z \subseteq dom F \to (S Fr ran F \to (z \neq \emptyset \to \exists w \in z \forall v \in z \neg v R w)))$
62	61	com23	$⊢ Fun F \to (S Fr ran F \to (z \subseteq dom F \to (z \neq \emptyset \to \exists w \in z \forall v \in z \neg v R w)))$
63	62	imp4a	$⊢ Fun F \to (S Fr ran F \to ((z \subseteq dom F \land z \neq \emptyset) \to \exists w \in z \forall v \in z \neg v R w))$
64	63	alrimdv	$⊢ Fun F \to (S Fr ran F \to \forall z ((z \subseteq dom F \land z \neq \emptyset) \to \exists w \in z \forall v \in z \neg v R w))$
65		df-fr	$⊢ R Fr dom F \leftrightarrow \forall z ((z \subseteq dom F \land z \neq \emptyset) \to \exists w \in z \forall v \in z \neg v R w)$
66	64 65	imbitrrdi	$⊢ Fun F \to (S Fr ran F \to R Fr dom F)$
67		freq2	$⊢ dom F = A \to (R Fr dom F \leftrightarrow R Fr A)$
68	67	biimpd	$⊢ dom F = A \to (R Fr dom F \to R Fr A)$
69	66 68	sylan9	$⊢ (Fun F \land dom F = A) \to (S Fr ran F \to R Fr A)$
70	6 69	sylbi	$⊢ F Fn A \to (S Fr ran F \to R Fr A)$
71	5 70	sylan9r	$⊢ (F Fn A \land ran F = B) \to (S Fr B \to R Fr A)$
72	3 71	sylbi	$⊢ F : A \underset{onto}{⟶} B \to (S Fr B \to R Fr A)$
73	2 72	syl	$⊢ F : A \underset{1-1 onto}{⟶} B \to (S Fr B \to R Fr A)$
74		df-f1o	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F : A \underset{1-1}{⟶} B \land F : A \underset{onto}{⟶} B)$
75		fveq2	$⊢ x = w \to F (x) = F (w)$
76	75	breq1d	$⊢ x = w \to (F (x) S F (y) \leftrightarrow F (w) S F (y))$
77		fveq2	$⊢ y = v \to F (y) = F (v)$
78	77	breq2d	$⊢ y = v \to (F (w) S F (y) \leftrightarrow F (w) S F (v))$
79	35 34 76 78 1	brab	$⊢ w R v \leftrightarrow F (w) S F (v)$
80	79	a1i	$⊢ (F : A \underset{1-1}{⟶} B \land (w \in A \land v \in A)) \to (w R v \leftrightarrow F (w) S F (v))$
81		f1fveq	$⊢ (F : A \underset{1-1}{⟶} B \land (w \in A \land v \in A)) \to (F (w) = F (v) \leftrightarrow w = v)$
82	81	bicomd	$⊢ (F : A \underset{1-1}{⟶} B \land (w \in A \land v \in A)) \to (w = v \leftrightarrow F (w) = F (v))$
83	40	a1i	$⊢ (F : A \underset{1-1}{⟶} B \land (w \in A \land v \in A)) \to (v R w \leftrightarrow F (v) S F (w))$
84	80 82 83	3orbi123d	$⊢ (F : A \underset{1-1}{⟶} B \land (w \in A \land v \in A)) \to ((w R v \lor w = v \lor v R w) \leftrightarrow (F (w) S F (v) \lor F (w) = F (v) \lor F (v) S F (w)))$
85	84	2ralbidva	$⊢ F : A \underset{1-1}{⟶} B \to (\forall w \in A \forall v \in A (w R v \lor w = v \lor v R w) \leftrightarrow \forall w \in A \forall v \in A (F (w) S F (v) \lor F (w) = F (v) \lor F (v) S F (w)))$
86		breq1	$⊢ F (w) = u \to (F (w) S F (v) \leftrightarrow u S F (v))$
87		eqeq1	$⊢ F (w) = u \to (F (w) = F (v) \leftrightarrow u = F (v))$
88		breq2	$⊢ F (w) = u \to (F (v) S F (w) \leftrightarrow F (v) S u)$
89	86 87 88	3orbi123d	$⊢ F (w) = u \to ((F (w) S F (v) \lor F (w) = F (v) \lor F (v) S F (w)) \leftrightarrow (u S F (v) \lor u = F (v) \lor F (v) S u))$
90	89	ralbidv	$⊢ F (w) = u \to (\forall v \in A (F (w) S F (v) \lor F (w) = F (v) \lor F (v) S F (w)) \leftrightarrow \forall v \in A (u S F (v) \lor u = F (v) \lor F (v) S u))$
91	90	cbvfo	$⊢ F : A \underset{onto}{⟶} B \to (\forall w \in A \forall v \in A (F (w) S F (v) \lor F (w) = F (v) \lor F (v) S F (w)) \leftrightarrow \forall u \in B \forall v \in A (u S F (v) \lor u = F (v) \lor F (v) S u))$
92		breq2	$⊢ F (v) = f \to (u S F (v) \leftrightarrow u S f)$
93		eqeq2	$⊢ F (v) = f \to (u = F (v) \leftrightarrow u = f)$
94		breq1	$⊢ F (v) = f \to (F (v) S u \leftrightarrow f S u)$
95	92 93 94	3orbi123d	$⊢ F (v) = f \to ((u S F (v) \lor u = F (v) \lor F (v) S u) \leftrightarrow (u S f \lor u = f \lor f S u))$
96	95	cbvfo	$⊢ F : A \underset{onto}{⟶} B \to (\forall v \in A (u S F (v) \lor u = F (v) \lor F (v) S u) \leftrightarrow \forall f \in B (u S f \lor u = f \lor f S u))$
97	96	ralbidv	$⊢ F : A \underset{onto}{⟶} B \to (\forall u \in B \forall v \in A (u S F (v) \lor u = F (v) \lor F (v) S u) \leftrightarrow \forall u \in B \forall f \in B (u S f \lor u = f \lor f S u))$
98	91 97	bitrd	$⊢ F : A \underset{onto}{⟶} B \to (\forall w \in A \forall v \in A (F (w) S F (v) \lor F (w) = F (v) \lor F (v) S F (w)) \leftrightarrow \forall u \in B \forall f \in B (u S f \lor u = f \lor f S u))$
99	85 98	sylan9bb	$⊢ (F : A \underset{1-1}{⟶} B \land F : A \underset{onto}{⟶} B) \to (\forall w \in A \forall v \in A (w R v \lor w = v \lor v R w) \leftrightarrow \forall u \in B \forall f \in B (u S f \lor u = f \lor f S u))$
100	74 99	sylbi	$⊢ F : A \underset{1-1 onto}{⟶} B \to (\forall w \in A \forall v \in A (w R v \lor w = v \lor v R w) \leftrightarrow \forall u \in B \forall f \in B (u S f \lor u = f \lor f S u))$
101	100	biimprd	$⊢ F : A \underset{1-1 onto}{⟶} B \to (\forall u \in B \forall f \in B (u S f \lor u = f \lor f S u) \to \forall w \in A \forall v \in A (w R v \lor w = v \lor v R w))$
102	73 101	anim12d	$⊢ F : A \underset{1-1 onto}{⟶} B \to ((S Fr B \land \forall u \in B \forall f \in B (u S f \lor u = f \lor f S u)) \to (R Fr A \land \forall w \in A \forall v \in A (w R v \lor w = v \lor v R w)))$
103		dfwe2	$⊢ S We B \leftrightarrow (S Fr B \land \forall u \in B \forall f \in B (u S f \lor u = f \lor f S u))$
104		dfwe2	$⊢ R We A \leftrightarrow (R Fr A \land \forall w \in A \forall v \in A (w R v \lor w = v \lor v R w))$
105	102 103 104	3imtr4g	$⊢ F : A \underset{1-1 onto}{⟶} B \to (S We B \to R We A)$

Metamath Proof Explorer

Theorem f1oweALT

Proof