Theorem bnj142 12474

Description: First-order logic and set theory.

Hypothesis

Ref	Expression
bnj142.1	|- (F` A) e. _V

Assertion

Ref	Expression
bnj142	|- (F Fn {A} -> (u e. F -> u = <.A, (F` A)>.))

Proof of Theorem bnj142

Step	Hyp	Ref	Expression
1		elrel 4086	. . . . . 6 |- ((Rel F /\ u e. F) -> E.wE.z u = <.w, z>.)
2		fnrel 4511	. . . . . 6 |- (F Fn {A} -> Rel F)
3	1, 2	sylan 497	. . . . 5 |- ((F Fn {A} /\ u e. F) -> E.wE.z u = <.w, z>.)
4	3	pm4.71i 699	. . . 4 |- ((F Fn {A} /\ u e. F) <-> ((F Fn {A} /\ u e. F) /\ E.wE.z u = <.w, z>.))
5		anass 487	. . . 4 |- (((F Fn {A} /\ u e. F) /\ E.wE.z u = <.w, z>.) <-> (F Fn {A} /\ (u e. F /\ E.wE.z u = <.w, z>.)))
6	4, 5	bitr2i 191	. . 3 |- ((F Fn {A} /\ (u e. F /\ E.wE.z u = <.w, z>.)) <-> (F Fn {A} /\ u e. F))
7		eleq1 1957	. . . . . . . . 9 |- (u = <.w, z>. -> (u e. F <-> <.w, z>. e. F))
8	7	biimpac 462	. . . . . . . 8 |- ((u e. F /\ u = <.w, z>.) -> <.w, z>. e. F)
9	8	adantl 424	. . . . . . 7 |- ((F Fn {A} /\ (u e. F /\ u = <.w, z>.)) -> <.w, z>. e. F)
10		eqrel 4077	. . . . . . . . . . . 12 |- ((Rel F /\ Rel {<.x, y>. | (x = A /\ y = (F` A))}) -> (F = {<.x, y>. | (x = A /\ y = (F` A))} <-> A.wA.z(<.w, z>. e. F <-> <.w, z>. e. {<.x, y>. | (x = A /\ y = (F` A))})))
11		relopab 4104	. . . . . . . . . . . . 13 |- Rel {<.x, y>. | (x = A /\ y = (F` A))}
12		releq 4071	. . . . . . . . . . . . 13 |- (F = {<.x, y>. | (x = A /\ y = (F` A))} -> (Rel F <-> Rel {<.x, y>. | (x = A /\ y = (F` A))}))
13	11, 12	mpbiri 211	. . . . . . . . . . . 12 |- (F = {<.x, y>. | (x = A /\ y = (F` A))} -> Rel F)
14	10, 13, 11	sylancl 525	. . . . . . . . . . 11 |- (F = {<.x, y>. | (x = A /\ y = (F` A))} -> (F = {<.x, y>. | (x = A /\ y = (F` A))} <-> A.wA.z(<.w, z>. e. F <-> <.w, z>. e. {<.x, y>. | (x = A /\ y = (F` A))})))
15	14	ibi 652	. . . . . . . . . 10 |- (F = {<.x, y>. | (x = A /\ y = (F` A))} -> A.wA.z(<.w, z>. e. F <-> <.w, z>. e. {<.x, y>. | (x = A /\ y = (F` A))}))
16		bnj141 12473	. . . . . . . . . 10 |- (F Fn {A} <-> F = {<.x, y>. | (x = A /\ y = (F` A))})
17		bnj142.1	. . . . . . . . . . . . 13 |- (F` A) e. _V
18	17	bnj136 12468	. . . . . . . . . . . 12 |- (<.w, z>. = <.A, (F` A)>. <-> <.w, z>. e. {<.x, y>. | (x = A /\ y = (F` A))})
19	18	bibi2i 669	. . . . . . . . . . 11 |- ((<.w, z>. e. F <-> <.w, z>. = <.A, (F` A)>.) <-> (<.w, z>. e. F <-> <.w, z>. e. {<.x, y>. | (x = A /\ y = (F` A))}))
20	19	2albii 1347	. . . . . . . . . 10 |- (A.wA.z(<.w, z>. e. F <-> <.w, z>. = <.A, (F` A)>.) <-> A.wA.z(<.w, z>. e. F <-> <.w, z>. e. {<.x, y>. | (x = A /\ y = (F` A))}))
21	15, 16, 20	3imtr4i 236	. . . . . . . . 9 |- (F Fn {A} -> A.wA.z(<.w, z>. e. F <-> <.w, z>. = <.A, (F` A)>.))
22	21	19.21bbi 1409	. . . . . . . 8 |- (F Fn {A} -> (<.w, z>. e. F <-> <.w, z>. = <.A, (F` A)>.))
23	22	adantr 425	. . . . . . 7 |- ((F Fn {A} /\ (u e. F /\ u = <.w, z>.)) -> (<.w, z>. e. F <-> <.w, z>. = <.A, (F` A)>.))
24	9, 23	mpbid 212	. . . . . 6 |- ((F Fn {A} /\ (u e. F /\ u = <.w, z>.)) -> <.w, z>. = <.A, (F` A)>.)
25		eqeq1 1890	. . . . . . 7 |- (u = <.w, z>. -> (u = <.A, (F` A)>. <-> <.w, z>. = <.A, (F` A)>.))
26	25	ad2antll 443	. . . . . 6 |- ((F Fn {A} /\ (u e. F /\ u = <.w, z>.)) -> (u = <.A, (F` A)>. <-> <.w, z>. = <.A, (F` A)>.))
27	24, 26	mpbird 213	. . . . 5 |- ((F Fn {A} /\ (u e. F /\ u = <.w, z>.)) -> u = <.A, (F` A)>.)
28	27	2eximi 1388	. . . 4 |- (E.wE.z(F Fn {A} /\ (u e. F /\ u = <.w, z>.)) -> E.wE.z u = <.A, (F` A)>.)
29		19.42v 1688	. . . . . . 7 |- (E.z(F Fn {A} /\ (u e. F /\ u = <.w, z>.)) <-> (F Fn {A} /\ E.z(u e. F /\ u = <.w, z>.)))
30		19.42v 1688	. . . . . . . 8 |- (E.z(u e. F /\ u = <.w, z>.) <-> (u e. F /\ E.z u = <.w, z>.))
31	30	anbi2i 538	. . . . . . 7 |- ((F Fn {A} /\ E.z(u e. F /\ u = <.w, z>.)) <-> (F Fn {A} /\ (u e. F /\ E.z u = <.w, z>.)))
32	29, 31	bitri 190	. . . . . 6 |- (E.z(F Fn {A} /\ (u e. F /\ u = <.w, z>.)) <-> (F Fn {A} /\ (u e. F /\ E.z u = <.w, z>.)))
33	32	exbii 1398	. . . . 5 |- (E.wE.z(F Fn {A} /\ (u e. F /\ u = <.w, z>.)) <-> E.w(F Fn {A} /\ (u e. F /\ E.z u = <.w, z>.)))
34		19.42v 1688	. . . . 5 |- (E.w(F Fn {A} /\ (u e. F /\ E.z u = <.w, z>.)) <-> (F Fn {A} /\ E.w(u e. F /\ E.z u = <.w, z>.)))
35		19.42v 1688	. . . . . 6 |- (E.w(u e. F /\ E.z u = <.w, z>.) <-> (u e. F /\ E.wE.z u = <.w, z>.))
36	35	anbi2i 538	. . . . 5 |- ((F Fn {A} /\ E.w(u e. F /\ E.z u = <.w, z>.)) <-> (F Fn {A} /\ (u e. F /\ E.wE.z u = <.w, z>.)))
37	33, 34, 36	3bitri 194	. . . 4 |- (E.wE.z(F Fn {A} /\ (u e. F /\ u = <.w, z>.)) <-> (F Fn {A} /\ (u e. F /\ E.wE.z u = <.w, z>.)))
38		19.9v 1662	. . . . 5 |- (E.wE.z u = <.A, (F` A)>. <-> E.z u = <.A, (F` A)>.)
39		19.9v 1662	. . . . 5 |- (E.z u = <.A, (F` A)>. <-> u = <.A, (F` A)>.)
40	38, 39	bitri 190	. . . 4 |- (E.wE.z u = <.A, (F` A)>. <-> u = <.A, (F` A)>.)
41	28, 37, 40	3imtr3i 235	. . 3 |- ((F Fn {A} /\ (u e. F /\ E.wE.z u = <.w, z>.)) -> u = <.A, (F` A)>.)
42	6, 41	sylbir 218	. 2 |- ((F Fn {A} /\ u e. F) -> u = <.A, (F` A)>.)
43	42	ex 402	1 |- (F Fn {A} -> (u e. F -> u = <.A, (F` A)>.))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  _Vcvv 2292  {csn 3044  <.cop 3046  {copab 3395  Rel wrel 3991   Fn wfn 3993  ` cfv 3998

This theorem is referenced by:  bnj145 12477

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014

Copyright terms: Public domain