Theorem f1oweALT 6784

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

Hypothesis

Ref	Expression
f1oweALT.1

Assertion

Ref	Expression
f1oweALT

Distinct variable groups:   ,,S   ,,

Proof of Theorem f1oweALT

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1ofo 5828	. . . 4
2		df-fo 5599	. . . . 5
3		freq2 4855	. . . . . . 7
4	3	biimprd 223	. . . . . 6
5		df-fn 5596	. . . . . . 7
6		df-fr 4843	. . . . . . . . . . . . . . . . . . . 20
7		vex 3112	. . . . . . . . . . . . . . . . . . . . . 22
8	7	funimaex 5671	. . . . . . . . . . . . . . . . . . . . 21
9		n0 3794	. . . . . . . . . . . . . . . . . . . . . . . . 25
10		funfvima2 6148	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
11		ne0i 3790	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
12	10, 11	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . 26
13	12	exlimdv 1724	. . . . . . . . . . . . . . . . . . . . . . . . 25
14	9, 13	syl5bi 217	. . . . . . . . . . . . . . . . . . . . . . . 24
15	14	imp 429	. . . . . . . . . . . . . . . . . . . . . . 23
16		imassrn 5353	. . . . . . . . . . . . . . . . . . . . . . 23
17	15, 16	jctil 537	. . . . . . . . . . . . . . . . . . . . . 22
18		sseq1 3524	. . . . . . . . . . . . . . . . . . . . . . . . 25
19		neeq1 2738	. . . . . . . . . . . . . . . . . . . . . . . . 25
20	18, 19	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . 24
21		raleq 3054	. . . . . . . . . . . . . . . . . . . . . . . . 25
22	21	rexeqbi1dv 3063	. . . . . . . . . . . . . . . . . . . . . . . 24
23	20, 22	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . 23
24	23	spcgv 3194	. . . . . . . . . . . . . . . . . . . . . 22
25	17, 24	syl7 68	. . . . . . . . . . . . . . . . . . . . 21
26	8, 25	syl 16	. . . . . . . . . . . . . . . . . . . 20
27	6, 26	syl5bi 217	. . . . . . . . . . . . . . . . . . 19
28	27	com23 78	. . . . . . . . . . . . . . . . . 18
29	28	expd 436	. . . . . . . . . . . . . . . . 17
30	29	anabsi5 817	. . . . . . . . . . . . . . . 16
31	30	impd 431	. . . . . . . . . . . . . . 15
32		fores 5809	. . . . . . . . . . . . . . . 16
33		fvres 5885	. . . . . . . . . . . . . . . . . . . . . 22
34		fvres 5885	. . . . . . . . . . . . . . . . . . . . . 22
35	33, 34	breqan12rd 4468	. . . . . . . . . . . . . . . . . . . . 21
36		vex 3112	. . . . . . . . . . . . . . . . . . . . . 22
37		vex 3112	. . . . . . . . . . . . . . . . . . . . . 22
38		fveq2 5871	. . . . . . . . . . . . . . . . . . . . . . 23
39	38	breq1d 4462	. . . . . . . . . . . . . . . . . . . . . 22
40		fveq2 5871	. . . . . . . . . . . . . . . . . . . . . . 23
41	40	breq2d 4464	. . . . . . . . . . . . . . . . . . . . . 22
42		f1oweALT.1	. . . . . . . . . . . . . . . . . . . . . 22
43	36, 37, 39, 41, 42	brab 4775	. . . . . . . . . . . . . . . . . . . . 21
44	35, 43	syl6rbbr 264	. . . . . . . . . . . . . . . . . . . 20
45	44	notbid 294	. . . . . . . . . . . . . . . . . . 19
46	45	ralbidva 2893	. . . . . . . . . . . . . . . . . 18
47	46	rexbiia 2958	. . . . . . . . . . . . . . . . 17
48		breq1 4455	. . . . . . . . . . . . . . . . . . . . 21
49	48	notbid 294	. . . . . . . . . . . . . . . . . . . 20
50	49	cbvfo 6192	. . . . . . . . . . . . . . . . . . 19
51	50	rexbidv 2968	. . . . . . . . . . . . . . . . . 18
52		breq2 4456	. . . . . . . . . . . . . . . . . . . . 21
53	52	notbid 294	. . . . . . . . . . . . . . . . . . . 20
54	53	ralbidv 2896	. . . . . . . . . . . . . . . . . . 19
55	54	cbvexfo 6193	. . . . . . . . . . . . . . . . . 18
56	51, 55	bitrd 253	. . . . . . . . . . . . . . . . 17
57	47, 56	syl5bb 257	. . . . . . . . . . . . . . . 16
58	32, 57	syl 16	. . . . . . . . . . . . . . 15
59	31, 58	sylibrd 234	. . . . . . . . . . . . . 14
60	59	exp4b 607	. . . . . . . . . . . . 13
61	60	com34 83	. . . . . . . . . . . 12
62	61	com23 78	. . . . . . . . . . 11
63	62	imp4a 589	. . . . . . . . . 10
64	63	alrimdv 1721	. . . . . . . . 9
65		df-fr 4843	. . . . . . . . 9
66	64, 65	syl6ibr 227	. . . . . . . 8
67		freq2 4855	. . . . . . . . 9
68	67	biimpd 207	. . . . . . . 8
69	66, 68	sylan9 657	. . . . . . 7
70	5, 69	sylbi 195	. . . . . 6
71	4, 70	sylan9r 658	. . . . 5
72	2, 71	sylbi 195	. . . 4
73	1, 72	syl 16	. . 3
74		df-f1o 5600	. . . . 5
75		fveq2 5871	. . . . . . . . . . 11
76	75	breq1d 4462	. . . . . . . . . 10
77		fveq2 5871	. . . . . . . . . . 11
78	77	breq2d 4464	. . . . . . . . . 10
79	37, 36, 76, 78, 42	brab 4775	. . . . . . . . 9
80	79	a1i 11	. . . . . . . 8
81		f1fveq 6170	. . . . . . . . 9
82	81	bicomd 201	. . . . . . . 8
83	43	a1i 11	. . . . . . . 8
84	80, 82, 83	3orbi123d 1298	. . . . . . 7
85	84	2ralbidva 2899	. . . . . 6
86		breq1 4455	. . . . . . . . . 10
87		eqeq1 2461	. . . . . . . . . 10
88		breq2 4456	. . . . . . . . . 10
89	86, 87, 88	3orbi123d 1298	. . . . . . . . 9
90	89	ralbidv 2896	. . . . . . . 8
91	90	cbvfo 6192	. . . . . . 7
92		breq2 4456	. . . . . . . . . 10
93		eqeq2 2472	. . . . . . . . . 10
94		breq1 4455	. . . . . . . . . 10
95	92, 93, 94	3orbi123d 1298	. . . . . . . . 9
96	95	cbvfo 6192	. . . . . . . 8
97	96	ralbidv 2896	. . . . . . 7
98	91, 97	bitrd 253	. . . . . 6
99	85, 98	sylan9bb 699	. . . . 5
100	74, 99	sylbi 195	. . . 4
101	100	biimprd 223	. . 3
102	73, 101	anim12d 563	. 2
103		dfwe2 6617	. 2
104		dfwe2 6617	. 2
105	102, 103, 104	3imtr4g 270	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  \/w3o 972  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  =/=wne 2652  A.wral 2807  E.wrex 2808  cvv 3109  C_wss 3475  c0 3784   class class class wbr 4452  {copab 4509  Frwfr 4840  Wewwe 4842  domcdm 5004  rancrn 5005  |`cres 5006  "cima 5007  Funwfun 5587  Fnwfn 5588  -1-1->wf1 5590  -onto->wfo 5591  -1-1-onto->wf1o 5592  `cfv 5593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pr 4691  ax-un 6592

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601