Theorem repfuntw 14502

Description: Representation as a set of pairs of a function whose domain has two distinct elements.

Hypotheses

Ref	Expression
repfuntw.1	|- I e. A
repfuntw.2	|- J e. B

Assertion

Ref	Expression
repfuntw	|- (I =/= J -> (F Fn {I, J} <-> F = {<.I, (F` I)>., <.J, (F` J)>.}))

Proof of Theorem repfuntw

Step	Hyp	Ref	Expression
1		elprg 3060	. . . . . . 7 |- (x e. {I, J} -> (x e. {I, J} <-> (x = I \/ x = J)))
2		fveq2 4681	. . . . . . . . . 10 |- (x = I -> (F` x) = (F` I))
3		fveq2 4681	. . . . . . . . . 10 |- (x = I -> ({<.I, (F` I)>., <.J, (F` J)>.}` x) = ({<.I, (F` I)>., <.J, (F` J)>.}` I))
4	2, 3	eqeq12d 1899	. . . . . . . . 9 |- (x = I -> ((F` x) = ({<.I, (F` I)>., <.J, (F` J)>.}` x) <-> (F` I) = ({<.I, (F` I)>., <.J, (F` J)>.}` I)))
5		dmsnop 4367	. . . . . . . . . . . . . . 15 |- dom {<.J, (F` J)>.} = {J}
6		ineq1 2789	. . . . . . . . . . . . . . . 16 |- (dom {<.J, (F` J)>.} = {J} -> (dom {<.J, (F` J)>.} i^i {I}) = ({J} i^i {I}))
7		eqeq1 1890	. . . . . . . . . . . . . . . . 17 |- ((dom {<.J, (F` J)>.} i^i {I}) = ({J} i^i {I}) -> ((dom {<.J, (F` J)>.} i^i {I}) = (/) <-> ({J} i^i {I}) = (/)))
8		necom 2094	. . . . . . . . . . . . . . . . . 18 |- (I =/= J <-> J =/= I)
9		disjsn2 3091	. . . . . . . . . . . . . . . . . 18 |- (J =/= I -> ({J} i^i {I}) = (/))
10	8, 9	sylbi 216	. . . . . . . . . . . . . . . . 17 |- (I =/= J -> ({J} i^i {I}) = (/))
11	7, 10	syl5bir 227	. . . . . . . . . . . . . . . 16 |- ((dom {<.J, (F` J)>.} i^i {I}) = ({J} i^i {I}) -> (I =/= J -> (dom {<.J, (F` J)>.} i^i {I}) = (/)))
12	6, 11	syl 12	. . . . . . . . . . . . . . 15 |- (dom {<.J, (F` J)>.} = {J} -> (I =/= J -> (dom {<.J, (F` J)>.} i^i {I}) = (/)))
13	5, 12	ax-mp 7	. . . . . . . . . . . . . 14 |- (I =/= J -> (dom {<.J, (F` J)>.} i^i {I}) = (/))
14	13	adantr 425	. . . . . . . . . . . . 13 |- ((I =/= J /\ F Fn {I, J}) -> (dom {<.J, (F` J)>.} i^i {I}) = (/))
15		imadisj 4285	. . . . . . . . . . . . 13 |- (({<.J, (F` J)>.}"{I}) = (/) <-> (dom {<.J, (F` J)>.} i^i {I}) = (/))
16	14, 15	sylibr 217	. . . . . . . . . . . 12 |- ((I =/= J /\ F Fn {I, J}) -> ({<.J, (F` J)>.}"{I}) = (/))
17		uneq2 2749	. . . . . . . . . . . . . . . . 17 |- (({<.J, (F` J)>.}"{I}) = (/) -> (({<.I, (F` I)>.}"{I}) u. ({<.J, (F` J)>.}"{I})) = (({<.I, (F` I)>.}"{I}) u. (/)))
18		un0 2896	. . . . . . . . . . . . . . . . 17 |- (({<.I, (F` I)>.}"{I}) u. (/)) = ({<.I, (F` I)>.}"{I})
19	17, 18	syl6eq 1944	. . . . . . . . . . . . . . . 16 |- (({<.J, (F` J)>.}"{I}) = (/) -> (({<.I, (F` I)>.}"{I}) u. ({<.J, (F` J)>.}"{I})) = ({<.I, (F` I)>.}"{I}))
20	19	eqeq1d 1892	. . . . . . . . . . . . . . 15 |- (({<.J, (F` J)>.}"{I}) = (/) -> ((({<.I, (F` I)>.}"{I}) u. ({<.J, (F` J)>.}"{I})) = {x} <-> ({<.I, (F` I)>.}"{I}) = {x}))
21	20	abbidv 2008	. . . . . . . . . . . . . 14 |- (({<.J, (F` J)>.}"{I}) = (/) -> {x | (({<.I, (F` I)>.}"{I}) u. ({<.J, (F` J)>.}"{I})) = {x}} = {x | ({<.I, (F` I)>.}"{I}) = {x}})
22	21	unieqd 3188	. . . . . . . . . . . . 13 |- (({<.J, (F` J)>.}"{I}) = (/) -> U.{x | (({<.I, (F` I)>.}"{I}) u. ({<.J, (F` J)>.}"{I})) = {x}} = U.{x | ({<.I, (F` I)>.}"{I}) = {x}})
23		repfuntw.1	. . . . . . . . . . . . . . . 16 |- I e. A
24	23	elisseti 2301	. . . . . . . . . . . . . . 15 |- I e. _V
25		fvex 4689	. . . . . . . . . . . . . . 15 |- (F` I) e. _V
26	24, 25	fvsn 4758	. . . . . . . . . . . . . 14 |- ({<.I, (F` I)>.}` I) = (F` I)
27		df-fv 4014	. . . . . . . . . . . . . 14 |- ({<.I, (F` I)>.}` I) = U.{x | ({<.I, (F` I)>.}"{I}) = {x}}
28	26, 27	eqtr3i 1910	. . . . . . . . . . . . 13 |- (F` I) = U.{x | ({<.I, (F` I)>.}"{I}) = {x}}
29	22, 28	syl6reqr 1947	. . . . . . . . . . . 12 |- (({<.J, (F` J)>.}"{I}) = (/) -> (F` I) = U.{x | (({<.I, (F` I)>.}"{I}) u. ({<.J, (F` J)>.}"{I})) = {x}})
30	16, 29	syl 12	. . . . . . . . . . 11 |- ((I =/= J /\ F Fn {I, J}) -> (F` I) = U.{x | (({<.I, (F` I)>.}"{I}) u. ({<.J, (F` J)>.}"{I})) = {x}})
31		imaundir 4329	. . . . . . . . . . . . . . 15 |- (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{I}) = (({<.I, (F` I)>.}"{I}) u. ({<.J, (F` J)>.}"{I}))
32	31	eqcomi 1888	. . . . . . . . . . . . . 14 |- (({<.I, (F` I)>.}"{I}) u. ({<.J, (F` J)>.}"{I})) = (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{I})
33	32	eqeq1i 1891	. . . . . . . . . . . . 13 |- ((({<.I, (F` I)>.}"{I}) u. ({<.J, (F` J)>.}"{I})) = {x} <-> (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{I}) = {x})
34	33	abbii 2006	. . . . . . . . . . . 12 |- {x | (({<.I, (F` I)>.}"{I}) u. ({<.J, (F` J)>.}"{I})) = {x}} = {x | (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{I}) = {x}}
35	34	unieqi 3187	. . . . . . . . . . 11 |- U.{x | (({<.I, (F` I)>.}"{I}) u. ({<.J, (F` J)>.}"{I})) = {x}} = U.{x | (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{I}) = {x}}
36	30, 35	syl6eq 1944	. . . . . . . . . 10 |- ((I =/= J /\ F Fn {I, J}) -> (F` I) = U.{x | (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{I}) = {x}})
37		df-fv 4014	. . . . . . . . . . . 12 |- (({<.I, (F` I)>.} u. {<.J, (F` J)>.})` I) = U.{x | (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{I}) = {x}}
38	37	eqcomi 1888	. . . . . . . . . . 11 |- U.{x | (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{I}) = {x}} = (({<.I, (F` I)>.} u. {<.J, (F` J)>.})` I)
39	38	a1i 8	. . . . . . . . . 10 |- ((I =/= J /\ F Fn {I, J}) -> U.{x | (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{I}) = {x}} = (({<.I, (F` I)>.} u. {<.J, (F` J)>.})` I))
40		df-pr 3050	. . . . . . . . . . . . 13 |- {<.I, (F` I)>., <.J, (F` J)>.} = ({<.I, (F` I)>.} u. {<.J, (F` J)>.})
41	40	eqcomi 1888	. . . . . . . . . . . 12 |- ({<.I, (F` I)>.} u. {<.J, (F` J)>.}) = {<.I, (F` I)>., <.J, (F` J)>.}
42	41	a1i 8	. . . . . . . . . . 11 |- ((I =/= J /\ F Fn {I, J}) -> ({<.I, (F` I)>.} u. {<.J, (F` J)>.}) = {<.I, (F` I)>., <.J, (F` J)>.})
43	42	fveq1d 4683	. . . . . . . . . 10 |- ((I =/= J /\ F Fn {I, J}) -> (({<.I, (F` I)>.} u. {<.J, (F` J)>.})` I) = ({<.I, (F` I)>., <.J, (F` J)>.}` I))
44	36, 39, 43	3eqtrd 1929	. . . . . . . . 9 |- ((I =/= J /\ F Fn {I, J}) -> (F` I) = ({<.I, (F` I)>., <.J, (F` J)>.}` I))
45	4, 44	syl5bir 227	. . . . . . . 8 |- (x = I -> ((I =/= J /\ F Fn {I, J}) -> (F` x) = ({<.I, (F` I)>., <.J, (F` J)>.}` x)))
46		fveq2 4681	. . . . . . . . . 10 |- (x = J -> (F` x) = (F` J))
47		fveq2 4681	. . . . . . . . . 10 |- (x = J -> ({<.I, (F` I)>., <.J, (F` J)>.}` x) = ({<.I, (F` I)>., <.J, (F` J)>.}` J))
48	46, 47	eqeq12d 1899	. . . . . . . . 9 |- (x = J -> ((F` x) = ({<.I, (F` I)>., <.J, (F` J)>.}` x) <-> (F` J) = ({<.I, (F` I)>., <.J, (F` J)>.}` J)))
49		dmsnop 4367	. . . . . . . . . . . . . . 15 |- dom {<.I, (F` I)>.} = {I}
50		ineq1 2789	. . . . . . . . . . . . . . . . 17 |- (dom {<.I, (F` I)>.} = {I} -> (dom {<.I, (F` I)>.} i^i {J}) = ({I} i^i {J}))
51		incom 2787	. . . . . . . . . . . . . . . . 17 |- ({I} i^i {J}) = ({J} i^i {I})
52	50, 51	syl6eq 1944	. . . . . . . . . . . . . . . 16 |- (dom {<.I, (F` I)>.} = {I} -> (dom {<.I, (F` I)>.} i^i {J}) = ({J} i^i {I}))
53		eqeq1 1890	. . . . . . . . . . . . . . . . 17 |- ((dom {<.I, (F` I)>.} i^i {J}) = ({J} i^i {I}) -> ((dom {<.I, (F` I)>.} i^i {J}) = (/) <-> ({J} i^i {I}) = (/)))
54	53, 10	syl5bir 227	. . . . . . . . . . . . . . . 16 |- ((dom {<.I, (F` I)>.} i^i {J}) = ({J} i^i {I}) -> (I =/= J -> (dom {<.I, (F` I)>.} i^i {J}) = (/)))
55	52, 54	syl 12	. . . . . . . . . . . . . . 15 |- (dom {<.I, (F` I)>.} = {I} -> (I =/= J -> (dom {<.I, (F` I)>.} i^i {J}) = (/)))
56	49, 55	ax-mp 7	. . . . . . . . . . . . . 14 |- (I =/= J -> (dom {<.I, (F` I)>.} i^i {J}) = (/))
57	56	adantr 425	. . . . . . . . . . . . 13 |- ((I =/= J /\ F Fn {I, J}) -> (dom {<.I, (F` I)>.} i^i {J}) = (/))
58		imadisj 4285	. . . . . . . . . . . . 13 |- (({<.I, (F` I)>.}"{J}) = (/) <-> (dom {<.I, (F` I)>.} i^i {J}) = (/))
59	57, 58	sylibr 217	. . . . . . . . . . . 12 |- ((I =/= J /\ F Fn {I, J}) -> ({<.I, (F` I)>.}"{J}) = (/))
60		uneq2 2749	. . . . . . . . . . . . . . . . 17 |- (({<.I, (F` I)>.}"{J}) = (/) -> (({<.J, (F` J)>.}"{J}) u. ({<.I, (F` I)>.}"{J})) = (({<.J, (F` J)>.}"{J}) u. (/)))
61		un0 2896	. . . . . . . . . . . . . . . . 17 |- (({<.J, (F` J)>.}"{J}) u. (/)) = ({<.J, (F` J)>.}"{J})
62	60, 61	syl6eq 1944	. . . . . . . . . . . . . . . 16 |- (({<.I, (F` I)>.}"{J}) = (/) -> (({<.J, (F` J)>.}"{J}) u. ({<.I, (F` I)>.}"{J})) = ({<.J, (F` J)>.}"{J}))
63	62	eqeq1d 1892	. . . . . . . . . . . . . . 15 |- (({<.I, (F` I)>.}"{J}) = (/) -> ((({<.J, (F` J)>.}"{J}) u. ({<.I, (F` I)>.}"{J})) = {x} <-> ({<.J, (F` J)>.}"{J}) = {x}))
64	63	abbidv 2008	. . . . . . . . . . . . . 14 |- (({<.I, (F` I)>.}"{J}) = (/) -> {x | (({<.J, (F` J)>.}"{J}) u. ({<.I, (F` I)>.}"{J})) = {x}} = {x | ({<.J, (F` J)>.}"{J}) = {x}})
65	64	unieqd 3188	. . . . . . . . . . . . 13 |- (({<.I, (F` I)>.}"{J}) = (/) -> U.{x | (({<.J, (F` J)>.}"{J}) u. ({<.I, (F` I)>.}"{J})) = {x}} = U.{x | ({<.J, (F` J)>.}"{J}) = {x}})
66		repfuntw.2	. . . . . . . . . . . . . . . 16 |- J e. B
67	66	elisseti 2301	. . . . . . . . . . . . . . 15 |- J e. _V
68		fvex 4689	. . . . . . . . . . . . . . 15 |- (F` J) e. _V
69	67, 68	fvsn 4758	. . . . . . . . . . . . . 14 |- ({<.J, (F` J)>.}` J) = (F` J)
70		df-fv 4014	. . . . . . . . . . . . . 14 |- ({<.J, (F` J)>.}` J) = U.{x | ({<.J, (F` J)>.}"{J}) = {x}}
71	69, 70	eqtr3i 1910	. . . . . . . . . . . . 13 |- (F` J) = U.{x | ({<.J, (F` J)>.}"{J}) = {x}}
72	65, 71	syl6reqr 1947	. . . . . . . . . . . 12 |- (({<.I, (F` I)>.}"{J}) = (/) -> (F` J) = U.{x | (({<.J, (F` J)>.}"{J}) u. ({<.I, (F` I)>.}"{J})) = {x}})
73	59, 72	syl 12	. . . . . . . . . . 11 |- ((I =/= J /\ F Fn {I, J}) -> (F` J) = U.{x | (({<.J, (F` J)>.}"{J}) u. ({<.I, (F` I)>.}"{J})) = {x}})
74		imaundir 4329	. . . . . . . . . . . . . . . 16 |- (({<.J, (F` J)>.} u. {<.I, (F` I)>.})"{J}) = (({<.J, (F` J)>.}"{J}) u. ({<.I, (F` I)>.}"{J}))
75	74	eqcomi 1888	. . . . . . . . . . . . . . 15 |- (({<.J, (F` J)>.}"{J}) u. ({<.I, (F` I)>.}"{J})) = (({<.J, (F` J)>.} u. {<.I, (F` I)>.})"{J})
76	75	eqeq1i 1891	. . . . . . . . . . . . . 14 |- ((({<.J, (F` J)>.}"{J}) u. ({<.I, (F` I)>.}"{J})) = {x} <-> (({<.J, (F` J)>.} u. {<.I, (F` I)>.})"{J}) = {x})
77	76	abbii 2006	. . . . . . . . . . . . 13 |- {x | (({<.J, (F` J)>.}"{J}) u. ({<.I, (F` I)>.}"{J})) = {x}} = {x | (({<.J, (F` J)>.} u. {<.I, (F` I)>.})"{J}) = {x}}
78	77	unieqi 3187	. . . . . . . . . . . 12 |- U.{x | (({<.J, (F` J)>.}"{J}) u. ({<.I, (F` I)>.}"{J})) = {x}} = U.{x | (({<.J, (F` J)>.} u. {<.I, (F` I)>.})"{J}) = {x}}
79	78	a1i 8	. . . . . . . . . . 11 |- ((I =/= J /\ F Fn {I, J}) -> U.{x | (({<.J, (F` J)>.}"{J}) u. ({<.I, (F` I)>.}"{J})) = {x}} = U.{x | (({<.J, (F` J)>.} u. {<.I, (F` I)>.})"{J}) = {x}})
80		uncom 2744	. . . . . . . . . . . . . . . 16 |- ({<.J, (F` J)>.} u. {<.I, (F` I)>.}) = ({<.I, (F` I)>.} u. {<.J, (F` J)>.})
81	80	imaeq1i 4261	. . . . . . . . . . . . . . 15 |- (({<.J, (F` J)>.} u. {<.I, (F` I)>.})"{J}) = (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{J})
82	81	eqeq1i 1891	. . . . . . . . . . . . . 14 |- ((({<.J, (F` J)>.} u. {<.I, (F` I)>.})"{J}) = {x} <-> (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{J}) = {x})
83	82	abbii 2006	. . . . . . . . . . . . 13 |- {x | (({<.J, (F` J)>.} u. {<.I, (F` I)>.})"{J}) = {x}} = {x | (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{J}) = {x}}
84	83	unieqi 3187	. . . . . . . . . . . 12 |- U.{x | (({<.J, (F` J)>.} u. {<.I, (F` I)>.})"{J}) = {x}} = U.{x | (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{J}) = {x}}
85	84	a1i 8	. . . . . . . . . . 11 |- ((I =/= J /\ F Fn {I, J}) -> U.{x | (({<.J, (F` J)>.} u. {<.I, (F` I)>.})"{J}) = {x}} = U.{x | (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{J}) = {x}})
86	73, 79, 85	3eqtrd 1929	. . . . . . . . . 10 |- ((I =/= J /\ F Fn {I, J}) -> (F` J) = U.{x | (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{J}) = {x}})
87		df-fv 4014	. . . . . . . . . . . 12 |- (({<.I, (F` I)>.} u. {<.J, (F` J)>.})` J) = U.{x | (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{J}) = {x}}
88	87	eqcomi 1888	. . . . . . . . . . 11 |- U.{x | (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{J}) = {x}} = (({<.I, (F` I)>.} u. {<.J, (F` J)>.})` J)
89	88	a1i 8	. . . . . . . . . 10 |- ((I =/= J /\ F Fn {I, J}) -> U.{x | (({<.I, (F` I)>.} u. {<.J, (F` J)>.})"{J}) = {x}} = (({<.I, (F` I)>.} u. {<.J, (F` J)>.})` J))
90	42	fveq1d 4683	. . . . . . . . . 10 |- ((I =/= J /\ F Fn {I, J}) -> (({<.I, (F` I)>.} u. {<.J, (F` J)>.})` J) = ({<.I, (F` I)>., <.J, (F` J)>.}` J))
91	86, 89, 90	3eqtrd 1929	. . . . . . . . 9 |- ((I =/= J /\ F Fn {I, J}) -> (F` J) = ({<.I, (F` I)>., <.J, (F` J)>.}` J))
92	48, 91	syl5bir 227	. . . . . . . 8 |- (x = J -> ((I =/= J /\ F Fn {I, J}) -> (F` x) = ({<.I, (F` I)>., <.J, (F` J)>.}` x)))
93	45, 92	jaoi 368	. . . . . . 7 |- ((x = I \/ x = J) -> ((I =/= J /\ F Fn {I, J}) -> (F` x) = ({<.I, (F` I)>., <.J, (F` J)>.}` x)))
94	1, 93	syl6bi 231	. . . . . 6 |- (x e. {I, J} -> (x e. {I, J} -> ((I =/= J /\ F Fn {I, J}) -> (F` x) = ({<.I, (F` I)>., <.J, (F` J)>.}` x))))
95	94	pm2.43i 78	. . . . 5 |- (x e. {I, J} -> ((I =/= J /\ F Fn {I, J}) -> (F` x) = ({<.I, (F` I)>., <.J, (F` J)>.}` x)))
96	95	com12 14	. . . 4 |- ((I =/= J /\ F Fn {I, J}) -> (x e. {I, J} -> (F` x) = ({<.I, (F` I)>., <.J, (F` J)>.}` x)))
97	96	r19.21aiv 2175	. . 3 |- ((I =/= J /\ F Fn {I, J}) -> A.x e. {I, J} (F` x) = ({<.I, (F` I)>., <.J, (F` J)>.}` x))
98		simpr 350	. . . 4 |- ((I =/= J /\ F Fn {I, J}) -> F Fn {I, J})
99	24, 67, 25, 68	funpr 4467	. . . . . . 7 |- (I =/= J -> Fun {<.I, (F` I)>., <.J, (F` J)>.})
100	40	dmeqi 4158	. . . . . . . 8 |- dom {<.I, (F` I)>., <.J, (F` J)>.} = dom ({<.I, (F` I)>.} u. {<.J, (F` J)>.})
101		dmun 4163	. . . . . . . 8 |- dom ({<.I, (F` I)>.} u. {<.J, (F` J)>.}) = (dom {<.I, (F` I)>.} u. dom {<.J, (F` J)>.})
102	49, 5	uneq12i 2753	. . . . . . . . 9 |- (dom {<.I, (F` I)>.} u. dom {<.J, (F` J)>.}) = ({I} u. {J})
103		df-pr 3050	. . . . . . . . 9 |- {I, J} = ({I} u. {J})
104	102, 103	eqtr4i 1911	. . . . . . . 8 |- (dom {<.I, (F` I)>.} u. dom {<.J, (F` J)>.}) = {I, J}
105	100, 101, 104	3eqtri 1912	. . . . . . 7 |- dom {<.I, (F` I)>., <.J, (F` J)>.} = {I, J}
106	99, 105	jctir 317	. . . . . 6 |- (I =/= J -> (Fun {<.I, (F` I)>., <.J, (F` J)>.} /\ dom {<.I, (F` I)>., <.J, (F` J)>.} = {I, J}))
107		df-fn 4009	. . . . . 6 |- ({<.I, (F` I)>., <.J, (F` J)>.} Fn {I, J} <-> (Fun {<.I, (F` I)>., <.J, (F` J)>.} /\ dom {<.I, (F` I)>., <.J, (F` J)>.} = {I, J}))
108	106, 107	sylibr 217	. . . . 5 |- (I =/= J -> {<.I, (F` I)>., <.J, (F` J)>.} Fn {I, J})
109	108	adantr 425	. . . 4 |- ((I =/= J /\ F Fn {I, J}) -> {<.I, (F` I)>., <.J, (F` J)>.} Fn {I, J})
110		eqfnfv2 4767	. . . 4 |- ((F Fn {I, J} /\ {<.I, (F` I)>., <.J, (F` J)>.} Fn {I, J}) -> (F = {<.I, (F` I)>., <.J, (F` J)>.} <-> A.x e. {I, J} (F` x) = ({<.I, (F` I)>., <.J, (F` J)>.}` x)))
111	98, 109, 110	syl11anc 524	. . 3 |- ((I =/= J /\ F Fn {I, J}) -> (F = {<.I, (F` I)>., <.J, (F` J)>.} <-> A.x e. {I, J} (F` x) = ({<.I, (F` I)>., <.J, (F` J)>.}` x)))
112	97, 111	mpbird 213	. 2 |- ((I =/= J /\ F Fn {I, J}) -> F = {<.I, (F` I)>., <.J, (F` J)>.})
113		df-fn 4009	. . 3 |- (F Fn {I, J} <-> (Fun F /\ dom F = {I, J}))
114	49	a1i 8	. . . . . . . . . 10 |- (I =/= J -> dom {<.I, (F` I)>.} = {I})
115	5	a1i 8	. . . . . . . . . 10 |- (I =/= J -> dom {<.J, (F` J)>.} = {J})
116	114, 115	ineq12d 2797	. . . . . . . . 9 |- (I =/= J -> (dom {<.I, (F` I)>.} i^i dom {<.J, (F` J)>.}) = ({I} i^i {J}))
117		disjsn2 3091	. . . . . . . . 9 |- (I =/= J -> ({I} i^i {J}) = (/))
118	116, 117	eqtrd 1925	. . . . . . . 8 |- (I =/= J -> (dom {<.I, (F` I)>.} i^i dom {<.J, (F` J)>.}) = (/))
119	24, 25	funsn 4463	. . . . . . . . 9 |- Fun {<.I, (F` I)>.}
120	67, 68	funsn 4463	. . . . . . . . 9 |- Fun {<.J, (F` J)>.}
121	119, 120	pm3.2i 307	. . . . . . . 8 |- (Fun {<.I, (F` I)>.} /\ Fun {<.J, (F` J)>.})
122	118, 121	jctil 316	. . . . . . 7 |- (I =/= J -> ((Fun {<.I, (F` I)>.} /\ Fun {<.J, (F` J)>.}) /\ (dom {<.I, (F` I)>.} i^i dom {<.J, (F` J)>.}) = (/)))
123		funun 4462	. . . . . . 7 |- (((Fun {<.I, (F` I)>.} /\ Fun {<.J, (F` J)>.}) /\ (dom {<.I, (F` I)>.} i^i dom {<.J, (F` J)>.}) = (/)) -> Fun ({<.I, (F` I)>.} u. {<.J, (F` J)>.}))
124		funeq 4441	. . . . . . . . . 10 |- (({<.I, (F` I)>.} u. {<.J, (F` J)>.}) = F -> (Fun ({<.I, (F` I)>.} u. {<.J, (F` J)>.}) <-> Fun F))
125	124	biimpd 170	. . . . . . . . 9 |- (({<.I, (F` I)>.} u. {<.J, (F` J)>.}) = F -> (Fun ({<.I, (F` I)>.} u. {<.J, (F` J)>.}) -> Fun F))
126	125	eqcoms 1887	. . . . . . . 8 |- (F = ({<.I, (F` I)>.} u. {<.J, (F` J)>.}) -> (Fun ({<.I, (F` I)>.} u. {<.J, (F` J)>.}) -> Fun F))
127	126	com12 14	. . . . . . 7 |- (Fun ({<.I, (F` I)>.} u. {<.J, (F` J)>.}) -> (F = ({<.I, (F` I)>.} u. {<.J, (F` J)>.}) -> Fun F))
128	122, 123, 127	3syl 24	. . . . . 6 |- (I =/= J -> (F = ({<.I, (F` I)>.} u. {<.J, (F` J)>.}) -> Fun F))
129		eqtr 1904	. . . . . 6 |- ((F = {<.I, (F` I)>., <.J, (F` J)>.} /\ {<.I, (F` I)>., <.J, (F` J)>.} = ({<.I, (F` I)>.} u. {<.J, (F` J)>.})) -> F = ({<.I, (F` I)>.} u. {<.J, (F` J)>.}))
130	128, 129	syl5com 63	. . . . 5 |- ((F = {<.I, (F` I)>., <.J, (F` J)>.} /\ {<.I, (F` I)>., <.J, (F` J)>.} = ({<.I, (F` I)>.} u. {<.J, (F` J)>.})) -> (I =/= J -> Fun F))
131	40, 130	mpan2 760	. . . 4 |- (F = {<.I, (F` I)>., <.J, (F` J)>.} -> (I =/= J -> Fun F))
132	131	impcom 378	. . 3 |- ((I =/= J /\ F = {<.I, (F` I)>., <.J, (F` J)>.}) -> Fun F)
133		dmeq 4157	. . . . 5 |- (F = {<.I, (F` I)>., <.J, (F` J)>.} -> dom F = dom {<.I, (F` I)>., <.J, (F` J)>.})
134	133, 105	syl6eq 1944	. . . 4 |- (F = {<.I, (F` I)>., <.J, (F` J)>.} -> dom F = {I, J})
135	134	adantl 424	. . 3 |- ((I =/= J /\ F = {<.I, (F` I)>., <.J, (F` J)>.}) -> dom F = {I, J})
136	113, 132, 135	sylanbrc 527	. 2 |- ((I =/= J /\ F = {<.I, (F` I)>., <.J, (F` J)>.}) -> F Fn {I, J})
137	112, 136	impbida 577	1 |- (I =/= J -> (F Fn {I, J} <-> F = {<.I, (F` I)>., <.J, (F` J)>.}))

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   = wceq 1298   e. wcel 1300  {cab 1871   =/= wne 2017  A.wral 2105   u. cun 2591   i^i cin 2592  (/)c0 2875  {csn 3044  {cpr 3045  <.cop 3046  U.cuni 3177  dom cdm 3986  "cima 3989  Fun wfun 3992   Fn wfn 3993  ` cfv 3998

This theorem is referenced by:  repcpwti 14503

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-3an 860  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