Theorem brtpos2 5807

Description: Value of the transposition at a pair <.A , B >.. (Contributed by Mario Carneiro, 10-Sep-2015.)

Assertion

Ref	Expression
brtpos2	|- (B e. V -> (Atpos FB <-> (A e. ( `' dom F u. { (/) }) /\ U. `' {A } FB)))

Proof of Theorem brtpos2

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

Step	Hyp	Ref	Expression
1		reltpos 5806	. . . 4 |- Rel tpos F
2	1	brrelexi 4327	. . 3 |- (Atpos FB -> A e. _V)
3	2	a1i 9	. 2 |- (B e. V -> (Atpos FB -> A e. _V))
4		elex 2560	. . . 4 |- (A e. ( `' dom F u. { (/) }) -> A e. _V)
5	4	adantr 261	. . 3 |- ((A e. ( `' dom F u. { (/) }) /\ U. `' {A } FB) -> A e. _V)
6	5	a1i 9	. 2 |- (B e. V -> ((A e. ( `' dom F u. { (/) }) /\ U. `' {A } FB) -> A e. _V))
7		df-tpos 5801	. . . . . 6 |- tpos F = ( F o. (x e. ( `' dom F u. { (/) }) |-> U. `' {x }))
8	7	breqi 3761	. . . . 5 |- (Atpos FB <-> A( F o. (x e. ( `' dom F u. { (/) }) |-> U. `' {x }))B)
9		brcog 4445	. . . . 5 |- ((A e. _V /\ B e. V) -> (A( F o. (x e. ( `' dom F u. { (/) }) |-> U. `' {x }))B <-> E.y(A(x e. ( `' dom F u. { (/) }) |-> U. `' {x })y /\ y FB)))
10	8, 9	syl5bb 181	. . . 4 |- ((A e. _V /\ B e. V) -> (Atpos FB <-> E.y(A(x e. ( `' dom F u. { (/) }) |-> U. `' {x })y /\ y FB)))
11		funmpt 4881	. . . . . . . . . . 11 |- Fun (x e. ( `' dom F u. { (/) }) |-> U. `' {x })
12		funbrfv2b 5161	. . . . . . . . . . 11 |- ( Fun (x e. ( `' dom F u. { (/) }) |-> U. `' {x }) -> (A(x e. ( `' dom F u. { (/) }) |-> U. `' {x })y <-> (A e. dom (x e. ( `' dom F u. { (/) }) |-> U. `' {x }) /\ ((x e. ( `' dom F u. { (/) }) |-> U. `' {x }) ` A) = y)))
13	11, 12	ax-mp 7	. . . . . . . . . 10 |- (A(x e. ( `' dom F u. { (/) }) |-> U. `' {x })y <-> (A e. dom (x e. ( `' dom F u. { (/) }) |-> U. `' {x }) /\ ((x e. ( `' dom F u. { (/) }) |-> U. `' {x }) ` A) = y))
14		vex 2554	. . . . . . . . . . . . . . . . 17 |- x e. _V
15		snexg 3927	. . . . . . . . . . . . . . . . 17 |- (x e. _V -> {x } e. _V)
16	14, 15	ax-mp 7	. . . . . . . . . . . . . . . 16 |- {x } e. _V
17	16	cnvex 4799	. . . . . . . . . . . . . . 15 |- `' {x } e. _V
18	17	uniex 4140	. . . . . . . . . . . . . 14 |- U. `' {x } e. _V
19		eqid 2037	. . . . . . . . . . . . . 14 |- (x e. ( `' dom F u. { (/) }) |-> U. `' {x }) = (x e. ( `' dom F u. { (/) }) |-> U. `' {x })
20	18, 19	dmmpti 4971	. . . . . . . . . . . . 13 |- dom (x e. ( `' dom F u. { (/) }) |-> U. `' {x }) = ( `' dom F u. { (/) })
21	20	eleq2i 2101	. . . . . . . . . . . 12 |- (A e. dom (x e. ( `' dom F u. { (/) }) |-> U. `' {x }) <-> A e. ( `' dom F u. { (/) }))
22		eqcom 2039	. . . . . . . . . . . 12 |- (((x e. ( `' dom F u. { (/) }) |-> U. `' {x }) ` A) = y <-> y = ((x e. ( `' dom F u. { (/) }) |-> U. `' {x }) ` A))
23	21, 22	anbi12i 433	. . . . . . . . . . 11 |- ((A e. dom (x e. ( `' dom F u. { (/) }) |-> U. `' {x }) /\ ((x e. ( `' dom F u. { (/) }) |-> U. `' {x }) ` A) = y) <-> (A e. ( `' dom F u. { (/) }) /\ y = ((x e. ( `' dom F u. { (/) }) |-> U. `' {x }) ` A)))
24		snexg 3927	. . . . . . . . . . . . . . . 16 |- (A e. ( `' dom F u. { (/) }) -> {A } e. _V)
25		cnvexg 4798	. . . . . . . . . . . . . . . 16 |- ( {A } e. _V -> `' {A } e. _V)
26	24, 25	syl 14	. . . . . . . . . . . . . . 15 |- (A e. ( `' dom F u. { (/) }) -> `' {A } e. _V)
27		uniexg 4141	. . . . . . . . . . . . . . 15 |- ( `' {A } e. _V -> U. `' {A } e. _V)
28	26, 27	syl 14	. . . . . . . . . . . . . 14 |- (A e. ( `' dom F u. { (/) }) -> U. `' {A } e. _V)
29		sneq 3378	. . . . . . . . . . . . . . . . 17 |- (x = A -> {x } = {A })
30	29	cnveqd 4454	. . . . . . . . . . . . . . . 16 |- (x = A -> `' {x } = `' {A })
31	30	unieqd 3582	. . . . . . . . . . . . . . 15 |- (x = A -> U. `' {x } = U. `' {A })
32	31, 19	fvmptg 5191	. . . . . . . . . . . . . 14 |- ((A e. ( `' dom F u. { (/) }) /\ U. `' {A } e. _V) -> ((x e. ( `' dom F u. { (/) }) |-> U. `' {x }) ` A) = U. `' {A })
33	28, 32	mpdan 398	. . . . . . . . . . . . 13 |- (A e. ( `' dom F u. { (/) }) -> ((x e. ( `' dom F u. { (/) }) |-> U. `' {x }) ` A) = U. `' {A })
34	33	eqeq2d 2048	. . . . . . . . . . . 12 |- (A e. ( `' dom F u. { (/) }) -> (y = ((x e. ( `' dom F u. { (/) }) |-> U. `' {x }) ` A) <-> y = U. `' {A }))
35	34	pm5.32i 427	. . . . . . . . . . 11 |- ((A e. ( `' dom F u. { (/) }) /\ y = ((x e. ( `' dom F u. { (/) }) |-> U. `' {x }) ` A)) <-> (A e. ( `' dom F u. { (/) }) /\ y = U. `' {A }))
36	23, 35	bitri 173	. . . . . . . . . 10 |- ((A e. dom (x e. ( `' dom F u. { (/) }) |-> U. `' {x }) /\ ((x e. ( `' dom F u. { (/) }) |-> U. `' {x }) ` A) = y) <-> (A e. ( `' dom F u. { (/) }) /\ y = U. `' {A }))
37	13, 36	bitri 173	. . . . . . . . 9 |- (A(x e. ( `' dom F u. { (/) }) |-> U. `' {x })y <-> (A e. ( `' dom F u. { (/) }) /\ y = U. `' {A }))
38		ancom 253	. . . . . . . . 9 |- ((A e. ( `' dom F u. { (/) }) /\ y = U. `' {A }) <-> (y = U. `' {A } /\ A e. ( `' dom F u. { (/) })))
39	37, 38	bitri 173	. . . . . . . 8 |- (A(x e. ( `' dom F u. { (/) }) |-> U. `' {x })y <-> (y = U. `' {A } /\ A e. ( `' dom F u. { (/) })))
40	39	anbi1i 431	. . . . . . 7 |- ((A(x e. ( `' dom F u. { (/) }) |-> U. `' {x })y /\ y FB) <-> ((y = U. `' {A } /\ A e. ( `' dom F u. { (/) })) /\ y FB))
41		anass 381	. . . . . . 7 |- (((y = U. `' {A } /\ A e. ( `' dom F u. { (/) })) /\ y FB) <-> (y = U. `' {A } /\ (A e. ( `' dom F u. { (/) }) /\ y FB)))
42	40, 41	bitri 173	. . . . . 6 |- ((A(x e. ( `' dom F u. { (/) }) |-> U. `' {x })y /\ y FB) <-> (y = U. `' {A } /\ (A e. ( `' dom F u. { (/) }) /\ y FB)))
43	42	exbii 1493	. . . . 5 |- (E.y(A(x e. ( `' dom F u. { (/) }) |-> U. `' {x })y /\ y FB) <-> E.y(y = U. `' {A } /\ (A e. ( `' dom F u. { (/) }) /\ y FB)))
44		exsimpr 1506	. . . . . . 7 |- (E.y(y = U. `' {A } /\ (A e. ( `' dom F u. { (/) }) /\ y FB)) -> E.y(A e. ( `' dom F u. { (/) }) /\ y FB))
45		exsimpl 1505	. . . . . . . 8 |- (E.y(A e. ( `' dom F u. { (/) }) /\ y FB) -> E.y A e. ( `' dom F u. { (/) }))
46		19.9v 1748	. . . . . . . 8 |- (E.y A e. ( `' dom F u. { (/) }) <-> A e. ( `' dom F u. { (/) }))
47	45, 46	sylib 127	. . . . . . 7 |- (E.y(A e. ( `' dom F u. { (/) }) /\ y FB) -> A e. ( `' dom F u. { (/) }))
48	44, 47	syl 14	. . . . . 6 |- (E.y(y = U. `' {A } /\ (A e. ( `' dom F u. { (/) }) /\ y FB)) -> A e. ( `' dom F u. { (/) }))
49		simpl 102	. . . . . 6 |- ((A e. ( `' dom F u. { (/) }) /\ U. `' {A } FB) -> A e. ( `' dom F u. { (/) }))
50		breq1 3758	. . . . . . . . 9 |- (y = U. `' {A } -> (y FB <-> U. `' {A } FB))
51	50	anbi2d 437	. . . . . . . 8 |- (y = U. `' {A } -> ((A e. ( `' dom F u. { (/) }) /\ y FB) <-> (A e. ( `' dom F u. { (/) }) /\ U. `' {A } FB)))
52	51	ceqsexgv 2667	. . . . . . 7 |- ( U. `' {A } e. _V -> (E.y(y = U. `' {A } /\ (A e. ( `' dom F u. { (/) }) /\ y FB)) <-> (A e. ( `' dom F u. { (/) }) /\ U. `' {A } FB)))
53	28, 52	syl 14	. . . . . 6 |- (A e. ( `' dom F u. { (/) }) -> (E.y(y = U. `' {A } /\ (A e. ( `' dom F u. { (/) }) /\ y FB)) <-> (A e. ( `' dom F u. { (/) }) /\ U. `' {A } FB)))
54	48, 49, 53	pm5.21nii 619	. . . . 5 |- (E.y(y = U. `' {A } /\ (A e. ( `' dom F u. { (/) }) /\ y FB)) <-> (A e. ( `' dom F u. { (/) }) /\ U. `' {A } FB))
55	43, 54	bitri 173	. . . 4 |- (E.y(A(x e. ( `' dom F u. { (/) }) |-> U. `' {x })y /\ y FB) <-> (A e. ( `' dom F u. { (/) }) /\ U. `' {A } FB))
56	10, 55	syl6bb 185	. . 3 |- ((A e. _V /\ B e. V) -> (Atpos FB <-> (A e. ( `' dom F u. { (/) }) /\ U. `' {A } FB)))
57	56	expcom 109	. 2 |- (B e. V -> (A e. _V -> (Atpos FB <-> (A e. ( `' dom F u. { (/) }) /\ U. `' {A } FB))))
58	3, 6, 57	pm5.21ndd 620	1 |- (B e. V -> (Atpos FB <-> (A e. ( `' dom F u. { (/) }) /\ U. `' {A } FB)))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   = wceq 1242  E.wex 1378   e. wcel 1390   _Vcvv 2551   u. cun 2909   (/)c0 3218   {csn 3367   U.cuni 3571   class class class wbr 3755   |-> cmpt 3809   `'ccnv 4287   dom cdm 4288   o. ccom 4292   Fun wfun 4839   ` cfv 4845  tpos ctpos 5800

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-fv 4853  df-tpos 5801

This theorem is referenced by:  brtpos0  5808  reldmtpos  5809  brtposg  5810  dftpos4  5819  tpostpos  5820