Theorem cptarc 15242

Description: The cross product of two elements of a transitive Tarski's class is an element of the class. JFM CLASSES2 th. 67 (partly).

Assertion

Ref	Expression
cptarc	|- ((T e. Tarski /\ Tr T /\ (A e. T /\ B e. T)) -> (A X. B) e. T)

Proof of Theorem cptarc

Step	Hyp	Ref	Expression
1		xpeq1 4016	. . . . . . 7 |- (a = A -> (a X. b) = (A X. b))
2	1	eleq1d 1963	. . . . . 6 |- (a = A -> ((a X. b) e. T <-> (A X. b) e. T))
3	2	imbi2d 674	. . . . 5 |- (a = A -> ((Tr T -> (a X. b) e. T) <-> (Tr T -> (A X. b) e. T)))
4	3	imbi2d 674	. . . 4 |- (a = A -> ((T e. Tarski -> (Tr T -> (a X. b) e. T)) <-> (T e. Tarski -> (Tr T -> (A X. b) e. T))))
5		xpeq2 4017	. . . . . . 7 |- (b = B -> (A X. b) = (A X. B))
6	5	eleq1d 1963	. . . . . 6 |- (b = B -> ((A X. b) e. T <-> (A X. B) e. T))
7	6	imbi2d 674	. . . . 5 |- (b = B -> ((Tr T -> (A X. b) e. T) <-> (Tr T -> (A X. B) e. T)))
8	7	imbi2d 674	. . . 4 |- (b = B -> ((T e. Tarski -> (Tr T -> (A X. b) e. T)) <-> (T e. Tarski -> (Tr T -> (A X. B) e. T))))
9		ne0i 2881	. . . . . 6 |- (a e. T -> T =/= (/))
10		xpeq2 4017	. . . . . . . . 9 |- (b = (/) -> (a X. b) = (a X. (/)))
11		xp0 4334	. . . . . . . . . 10 |- (a X. (/)) = (/)
12		eqtr 1904	. . . . . . . . . 10 |- (((a X. b) = (a X. (/)) /\ (a X. (/)) = (/)) -> (a X. b) = (/))
13	11, 12	mpan2 760	. . . . . . . . 9 |- ((a X. b) = (a X. (/)) -> (a X. b) = (/))
14		eleq1 1957	. . . . . . . . . . . . 13 |- ((a X. b) = (/) -> ((a X. b) e. T <-> (/) e. T))
15		emptar 15231	. . . . . . . . . . . . . 14 |- ((T e. Tarski /\ T =/= (/)) -> (/) e. T)
16	15	ancoms 484	. . . . . . . . . . . . 13 |- ((T =/= (/) /\ T e. Tarski ) -> (/) e. T)
17	14, 16	syl5cbir 228	. . . . . . . . . . . 12 |- ((T =/= (/) /\ T e. Tarski ) -> ((a X. b) = (/) -> (a X. b) e. T))
18	17	3adant2 895	. . . . . . . . . . 11 |- ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) -> ((a X. b) = (/) -> (a X. b) e. T))
19	18	adantr 425	. . . . . . . . . 10 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) = (/) -> (a X. b) e. T))
20	19	com12 14	. . . . . . . . 9 |- ((a X. b) = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))
21	10, 13, 20	3syl 24	. . . . . . . 8 |- (b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))
22		df-ne 2019	. . . . . . . . . . . 12 |- (b =/= (/) <-> -. b = (/))
23		tarax3d2 15225	. . . . . . . . . . . . . . . . . . . . 21 |- ((T e. Tarski /\ a e. T) -> a ~< T)
24	23	expcom 403	. . . . . . . . . . . . . . . . . . . 20 |- (a e. T -> (T e. Tarski -> a ~< T))
25	24	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- ((a e. T /\ b e. T) -> (T e. Tarski -> a ~< T))
26	25	imp 377	. . . . . . . . . . . . . . . . . 18 |- (((a e. T /\ b e. T) /\ T e. Tarski ) -> a ~< T)
27	26	3adant1 894	. . . . . . . . . . . . . . . . 17 |- ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) -> a ~< T)
28	27	adantr 425	. . . . . . . . . . . . . . . 16 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> a ~< T)
29		elcartr 15238	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((T e. Tarski /\ Tr T /\ b e. T) -> b C_ T)
30		tarcrpr 15237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((T e. Tarski /\ a C_ T /\ b C_ T) -> (a X. b) C_ T)
31		ensdomtr 5534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((a X. b) ~~ a /\ a ~< T) -> (a X. b) ~< T)
32	31	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((a X. b) ~~ a -> (a ~< T -> (a X. b) ~< T))
33		tarax3f 15229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((T e. Tarski /\ (a X. b) C_ T /\ (a X. b) ~< T) -> (a X. b) e. T)
34	33	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (T e. Tarski -> ((a X. b) C_ T -> ((a X. b) ~< T -> (a X. b) e. T)))
35	34	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) -> ((a X. b) C_ T -> ((a X. b) ~< T -> (a X. b) e. T)))
36	35	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) C_ T -> ((a X. b) ~< T -> (a X. b) e. T)))
37	36	com3r 39	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((a X. b) ~< T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) C_ T -> (a X. b) e. T)))
38	32, 37	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((a X. b) ~~ a -> (a ~< T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) C_ T -> (a X. b) e. T))))
39	38	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((a X. b) ~~ a -> ((a X. b) C_ T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> (a X. b) e. T))))
40	39	com4l 43	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((a X. b) C_ T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T))))
41	30, 40	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((T e. Tarski /\ a C_ T /\ b C_ T) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T))))
42	41	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (T e. Tarski -> (a C_ T -> (b C_ T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T))))))
43	42	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a C_ T -> (b C_ T -> (T e. Tarski -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T))))))
44	43	com4r 45	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (T e. Tarski -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a C_ T -> (b C_ T -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T))))))
45	44	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a C_ T -> (b C_ T -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T))))))
46	45	anabsi5 553	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a C_ T -> (b C_ T -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T)))))
47	46	com13 37	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (b C_ T -> (a C_ T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T)))))
48	29, 47	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((T e. Tarski /\ Tr T /\ b e. T) -> (a C_ T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T)))))
49	48	3adant3l 1094	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((T e. Tarski /\ Tr T /\ (a e. T /\ b e. T)) -> (a C_ T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T)))))
50		elcartr 15238	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((T e. Tarski /\ Tr T /\ a e. T) -> a C_ T)
51	49, 50	syl5com 63	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((T e. Tarski /\ Tr T /\ a e. T) -> ((T e. Tarski /\ Tr T /\ (a e. T /\ b e. T)) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T)))))
52	51	3adant3r 1095	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((T e. Tarski /\ Tr T /\ (a e. T /\ b e. T)) -> ((T e. Tarski /\ Tr T /\ (a e. T /\ b e. T)) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T)))))
53	52	pm2.43i 78	. . . . . . . . . . . . . . . . . . . . . 22 |- ((T e. Tarski /\ Tr T /\ (a e. T /\ b e. T)) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T))))
54	53	3exp 1066	. . . . . . . . . . . . . . . . . . . . 21 |- (T e. Tarski -> (Tr T -> ((a e. T /\ b e. T) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T))))))
55	54	com3r 39	. . . . . . . . . . . . . . . . . . . 20 |- ((a e. T /\ b e. T) -> (T e. Tarski -> (Tr T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T))))))
56	55	imp 377	. . . . . . . . . . . . . . . . . . 19 |- (((a e. T /\ b e. T) /\ T e. Tarski ) -> (Tr T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T)))))
57	56	3adant1 894	. . . . . . . . . . . . . . . . . 18 |- ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) -> (Tr T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T)))))
58	57	imp 377	. . . . . . . . . . . . . . . . 17 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T))))
59	58	pm2.43i 78	. . . . . . . . . . . . . . . 16 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a ~< T -> ((a X. b) ~~ a -> (a X. b) e. T)))
60	28, 59	mpd 29	. . . . . . . . . . . . . . 15 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ a -> (a X. b) e. T))
61		visset 2295	. . . . . . . . . . . . . . . 16 |- a e. _V
62		visset 2295	. . . . . . . . . . . . . . . 16 |- b e. _V
63	61, 62	infxpabs 8839	. . . . . . . . . . . . . . 15 |- ((om ~<_ a /\ b =/= (/) /\ b ~<_ a) -> (a X. b) ~~ a)
64	60, 63	syl5com 63	. . . . . . . . . . . . . 14 |- ((om ~<_ a /\ b =/= (/) /\ b ~<_ a) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))
65	64	3exp 1066	. . . . . . . . . . . . 13 |- (om ~<_ a -> (b =/= (/) -> (b ~<_ a -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))))
66	65	com12 14	. . . . . . . . . . . 12 |- (b =/= (/) -> (om ~<_ a -> (b ~<_ a -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))))
67	22, 66	sylbir 218	. . . . . . . . . . 11 |- (-. b = (/) -> (om ~<_ a -> (b ~<_ a -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))))
68	67	com13 37	. . . . . . . . . 10 |- (b ~<_ a -> (om ~<_ a -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))))
69		domtri2 14433	. . . . . . . . . . . 12 |- ((b e. _V /\ a e. _V) -> (-. b ~<_ a <-> a ~< b))
70	62, 61, 69	mp2an 761	. . . . . . . . . . 11 |- (-. b ~<_ a <-> a ~< b)
71		sdomdom 5445	. . . . . . . . . . . 12 |- (a ~< b -> a ~<_ b)
72		domtr 5474	. . . . . . . . . . . . . . 15 |- ((om ~<_ a /\ a ~<_ b) -> om ~<_ b)
73	72	ex 402	. . . . . . . . . . . . . 14 |- (om ~<_ a -> (a ~<_ b -> om ~<_ b))
74		xpeq1 4016	. . . . . . . . . . . . . . . . . . . . . 22 |- (a = (/) -> (a X. b) = ((/) X. b))
75		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((a X. b) = ((/) X. b) -> ((a X. b) e. T <-> ((/) X. b) e. T))
76		xp0r 4065	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((/) X. b) = (/)
77	16, 76	syl5eqel 1975	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((T =/= (/) /\ T e. Tarski ) -> ((/) X. b) e. T)
78	75, 77	syl5bir 227	. . . . . . . . . . . . . . . . . . . . . 22 |- ((a X. b) = ((/) X. b) -> ((T =/= (/) /\ T e. Tarski ) -> (a X. b) e. T))
79	74, 78	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (a = (/) -> ((T =/= (/) /\ T e. Tarski ) -> (a X. b) e. T))
80	79	com12 14	. . . . . . . . . . . . . . . . . . . 20 |- ((T =/= (/) /\ T e. Tarski ) -> (a = (/) -> (a X. b) e. T))
81	80	3adant2 895	. . . . . . . . . . . . . . . . . . 19 |- ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) -> (a = (/) -> (a X. b) e. T))
82	81	adantr 425	. . . . . . . . . . . . . . . . . 18 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a = (/) -> (a X. b) e. T))
83	82	a1i12 9	. . . . . . . . . . . . . . . . 17 |- (om ~<_ b -> (a ~<_ b -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a = (/) -> (a X. b) e. T))))
84	83	com4r 45	. . . . . . . . . . . . . . . 16 |- (a = (/) -> (om ~<_ b -> (a ~<_ b -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))))
85		simpl3 881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> T e. Tarski )
86		simp2l3 977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((a X. b) C_ T /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) /\ (a X. b) ~~ b) -> T e. Tarski )
87		simp1 876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((a X. b) C_ T /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) /\ (a X. b) ~~ b) -> (a X. b) C_ T)
88		simpr 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) /\ (a X. b) ~~ b) -> (a X. b) ~~ b)
89		tarax3d2 15225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((T e. Tarski /\ b e. T) -> b ~< T)
90	89	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (b e. T -> (T e. Tarski -> b ~< T))
91	90	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((a e. T /\ b e. T) -> (T e. Tarski -> b ~< T))
92	91	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (((a e. T /\ b e. T) /\ T e. Tarski ) -> b ~< T)
93	92	3adant1 894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) -> b ~< T)
94	93	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) /\ (a X. b) ~~ b) -> b ~< T)
95		ensdomtr 5534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((a X. b) ~~ b /\ b ~< T) -> (a X. b) ~< T)
96	88, 94, 95	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) /\ (a X. b) ~~ b) -> (a X. b) ~< T)
97	96	3adant1 894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((a X. b) C_ T /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) /\ (a X. b) ~~ b) -> (a X. b) ~< T)
98	86, 87, 97, 33	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((a X. b) C_ T /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) /\ (a X. b) ~~ b) -> (a X. b) e. T)
99	98	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((a X. b) C_ T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T)))
100	30, 99	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((T e. Tarski /\ a C_ T /\ b C_ T) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T)))
101	100	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (T e. Tarski -> (a C_ T -> (b C_ T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T)))))
102	85, 101	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a C_ T -> (b C_ T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T)))))
103	102	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (b C_ T -> (a C_ T -> ((a X. b) ~~ b -> (a X. b) e. T)))))
104	103	pm2.43i 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (b C_ T -> (a C_ T -> ((a X. b) ~~ b -> (a X. b) e. T))))
105	104	com3l 38	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (b C_ T -> (a C_ T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T))))
106	29, 105	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((T e. Tarski /\ Tr T /\ b e. T) -> (a C_ T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T))))
107	106	3adant3l 1094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((T e. Tarski /\ Tr T /\ (a e. T /\ b e. T)) -> (a C_ T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T))))
108	107, 50	syl5com 63	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((T e. Tarski /\ Tr T /\ a e. T) -> ((T e. Tarski /\ Tr T /\ (a e. T /\ b e. T)) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T))))
109	108	3adant3r 1095	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((T e. Tarski /\ Tr T /\ (a e. T /\ b e. T)) -> ((T e. Tarski /\ Tr T /\ (a e. T /\ b e. T)) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T))))
110	109	pm2.43i 78	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((T e. Tarski /\ Tr T /\ (a e. T /\ b e. T)) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T)))
111	110	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (T e. Tarski -> (Tr T -> ((a e. T /\ b e. T) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T)))))
112	111	com3r 39	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((a e. T /\ b e. T) -> (T e. Tarski -> (Tr T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T)))))
113	112	imp 377	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((a e. T /\ b e. T) /\ T e. Tarski ) -> (Tr T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T))))
114	113	3adant1 894	. . . . . . . . . . . . . . . . . . . . . 22 |- ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) -> (Tr T -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T))))
115	114	imp 377	. . . . . . . . . . . . . . . . . . . . 21 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T)))
116	115	pm2.43i 78	. . . . . . . . . . . . . . . . . . . 20 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b -> (a X. b) e. T))
117		entr 5473	. . . . . . . . . . . . . . . . . . . 20 |- (((a X. b) ~~ (b X. a) /\ (b X. a) ~~ b) -> (a X. b) ~~ b)
118	116, 117	syl5com 63	. . . . . . . . . . . . . . . . . . 19 |- (((a X. b) ~~ (b X. a) /\ (b X. a) ~~ b) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))
119	61, 62	xpcomen 5498	. . . . . . . . . . . . . . . . . . 19 |- (a X. b) ~~ (b X. a)
120	62, 61	infxpabs 8839	. . . . . . . . . . . . . . . . . . 19 |- ((om ~<_ b /\ a =/= (/) /\ a ~<_ b) -> (b X. a) ~~ b)
121	118, 119, 120	sylancr 526	. . . . . . . . . . . . . . . . . 18 |- ((om ~<_ b /\ a =/= (/) /\ a ~<_ b) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))
122	121	3exp 1066	. . . . . . . . . . . . . . . . 17 |- (om ~<_ b -> (a =/= (/) -> (a ~<_ b -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))))
123	122	com12 14	. . . . . . . . . . . . . . . 16 |- (a =/= (/) -> (om ~<_ b -> (a ~<_ b -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))))
124	84, 123	pm2.61ine 2089	. . . . . . . . . . . . . . 15 |- (om ~<_ b -> (a ~<_ b -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T)))
125	124	a1dd 53	. . . . . . . . . . . . . 14 |- (om ~<_ b -> (a ~<_ b -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))))
126	73, 125	syl6 25	. . . . . . . . . . . . 13 |- (om ~<_ a -> (a ~<_ b -> (a ~<_ b -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T)))))
127	126	com13 37	. . . . . . . . . . . 12 |- (a ~<_ b -> (a ~<_ b -> (om ~<_ a -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T)))))
128	71, 71, 127	sylc 83	. . . . . . . . . . 11 |- (a ~< b -> (om ~<_ a -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))))
129	70, 128	sylbi 216	. . . . . . . . . 10 |- (-. b ~<_ a -> (om ~<_ a -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))))
130	68, 129	pm2.61i 140	. . . . . . . . 9 |- (om ~<_ a -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T)))
131		omex 5733	. . . . . . . . . . 11 |- om e. _V
132		domtri2 14433	. . . . . . . . . . 11 |- ((om e. _V /\ a e. _V) -> (-. om ~<_ a <-> a ~< om))
133	131, 61, 132	mp2an 761	. . . . . . . . . 10 |- (-. om ~<_ a <-> a ~< om)
134		simprl3 923	. . . . . . . . . . . . 13 |- (((om ~<_ b /\ a ~< om /\ -. b = (/)) /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T)) -> T e. Tarski )
135	50	3exp 1066	. . . . . . . . . . . . . . . . . . . . 21 |- (T e. Tarski -> (Tr T -> (a e. T -> a C_ T)))
136	135	com3r 39	. . . . . . . . . . . . . . . . . . . 20 |- (a e. T -> (T e. Tarski -> (Tr T -> a C_ T)))
137	136	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- ((a e. T /\ b e. T) -> (T e. Tarski -> (Tr T -> a C_ T)))
138	137	imp 377	. . . . . . . . . . . . . . . . . 18 |- (((a e. T /\ b e. T) /\ T e. Tarski ) -> (Tr T -> a C_ T))
139	138	3adant1 894	. . . . . . . . . . . . . . . . 17 |- ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) -> (Tr T -> a C_ T))
140	139	imp 377	. . . . . . . . . . . . . . . 16 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> a C_ T)
141	29	3exp 1066	. . . . . . . . . . . . . . . . . . . . 21 |- (T e. Tarski -> (Tr T -> (b e. T -> b C_ T)))
142	141	com3r 39	. . . . . . . . . . . . . . . . . . . 20 |- (b e. T -> (T e. Tarski -> (Tr T -> b C_ T)))
143	142	adantl 424	. . . . . . . . . . . . . . . . . . 19 |- ((a e. T /\ b e. T) -> (T e. Tarski -> (Tr T -> b C_ T)))
144	143	imp 377	. . . . . . . . . . . . . . . . . 18 |- (((a e. T /\ b e. T) /\ T e. Tarski ) -> (Tr T -> b C_ T))
145	144	3adant1 894	. . . . . . . . . . . . . . . . 17 |- ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) -> (Tr T -> b C_ T))
146	145	imp 377	. . . . . . . . . . . . . . . 16 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> b C_ T)
147	85, 140, 146	3jca 1050	. . . . . . . . . . . . . . 15 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (T e. Tarski /\ a C_ T /\ b C_ T))
148	147	adantl 424	. . . . . . . . . . . . . 14 |- (((om ~<_ b /\ a ~< om /\ -. b = (/)) /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T)) -> (T e. Tarski /\ a C_ T /\ b C_ T))
149	148, 30	syl 12	. . . . . . . . . . . . 13 |- (((om ~<_ b /\ a ~< om /\ -. b = (/)) /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T)) -> (a X. b) C_ T)
150		sdomdomtr 5532	. . . . . . . . . . . . . . . . . . . . 21 |- (b e. _V -> ((a ~< om /\ om ~<_ b) -> a ~< b))
151		eqtr 1904	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((a X. b) = ((/) X. b) /\ ((/) X. b) = (/)) -> (a X. b) = (/))
152		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((a X. b) = (/) -> ((a X. b) ~< T <-> (/) ~< T))
153		0sdomg 5529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (T e. Tarski -> ((/) ~< T <-> T =/= (/)))
154	153	biimpar 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((T e. Tarski /\ T =/= (/)) -> (/) ~< T)
155	152, 154	syl5cbir 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((T e. Tarski /\ T =/= (/)) -> ((a X. b) = (/) -> (a X. b) ~< T))
156	155	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((T =/= (/) /\ T e. Tarski ) -> ((a X. b) = (/) -> (a X. b) ~< T))
157	156	3adant2 895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) -> ((a X. b) = (/) -> (a X. b) ~< T))
158	157	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) = (/) -> (a X. b) ~< T))
159	158	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((a X. b) = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T))
160	159	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (b =/= (/) -> ((a X. b) = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T)))
161	160	a1i12 9	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (a ~< b -> ((a ~< om /\ om ~<_ b) -> (b =/= (/) -> ((a X. b) = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T)))))
162	161	com4r 45	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((a X. b) = (/) -> (a ~< b -> ((a ~< om /\ om ~<_ b) -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T)))))
163	151, 162	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((a X. b) = ((/) X. b) /\ ((/) X. b) = (/)) -> (a ~< b -> ((a ~< om /\ om ~<_ b) -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T)))))
164	163, 74, 76	sylancl 525	. . . . . . . . . . . . . . . . . . . . . 22 |- (a = (/) -> (a ~< b -> ((a ~< om /\ om ~<_ b) -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T)))))
165	93	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> b ~< T)
166	165	anim2i 362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((a X. b) ~~ b /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T)) -> ((a X. b) ~~ b /\ b ~< T))
167	166	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((a X. b) ~~ b -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~~ b /\ b ~< T)))
168	167, 95	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((a X. b) ~~ b -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T))
169	168	a1d 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((a X. b) ~~ b -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T)))
170	117, 169	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((a X. b) ~~ (b X. a) /\ (b X. a) ~~ b) -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T)))
171	170, 119, 120	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((om ~<_ b /\ a =/= (/) /\ a ~<_ b) -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T)))
172	171	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (om ~<_ b -> (a =/= (/) -> (a ~<_ b -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T)))))
173	172	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((a ~< om /\ om ~<_ b) -> (a =/= (/) -> (a ~<_ b -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T)))))
174	173	com3l 38	. . . . . . . . . . . . . . . . . . . . . . 23 |- (a =/= (/) -> (a ~<_ b -> ((a ~< om /\ om ~<_ b) -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T)))))
175	174, 71	syl5 20	. . . . . . . . . . . . . . . . . . . . . 22 |- (a =/= (/) -> (a ~< b -> ((a ~< om /\ om ~<_ b) -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T)))))
176	164, 175	pm2.61ine 2089	. . . . . . . . . . . . . . . . . . . . 21 |- (a ~< b -> ((a ~< om /\ om ~<_ b) -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T))))
177	150, 176	syl6 25	. . . . . . . . . . . . . . . . . . . 20 |- (b e. _V -> ((a ~< om /\ om ~<_ b) -> ((a ~< om /\ om ~<_ b) -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T)))))
178	62, 177	ax-mp 7	. . . . . . . . . . . . . . . . . . 19 |- ((a ~< om /\ om ~<_ b) -> ((a ~< om /\ om ~<_ b) -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T))))
179	178	pm2.43i 78	. . . . . . . . . . . . . . . . . 18 |- ((a ~< om /\ om ~<_ b) -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T)))
180	179	ex 402	. . . . . . . . . . . . . . . . 17 |- (a ~< om -> (om ~<_ b -> (b =/= (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T))))
181	180	com13 37	. . . . . . . . . . . . . . . 16 |- (b =/= (/) -> (om ~<_ b -> (a ~< om -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T))))
182	22, 181	sylbir 218	. . . . . . . . . . . . . . 15 |- (-. b = (/) -> (om ~<_ b -> (a ~< om -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T))))
183	182	com3l 38	. . . . . . . . . . . . . 14 |- (om ~<_ b -> (a ~< om -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) ~< T))))
184	183	3imp1 1081	. . . . . . . . . . . . 13 |- (((om ~<_ b /\ a ~< om /\ -. b = (/)) /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T)) -> (a X. b) ~< T)
185	134, 149, 184, 33	syl111anc 1100	. . . . . . . . . . . 12 |- (((om ~<_ b /\ a ~< om /\ -. b = (/)) /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T)) -> (a X. b) e. T)
186	185	3exp1 1084	. . . . . . . . . . 11 |- (om ~<_ b -> (a ~< om -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))))
187		domtri2 14433	. . . . . . . . . . . . 13 |- ((om e. _V /\ b e. _V) -> (-. om ~<_ b <-> b ~< om))
188	131, 62, 187	mp2an 761	. . . . . . . . . . . 12 |- (-. om ~<_ b <-> b ~< om)
189		cptwff 14436	. . . . . . . . . . . . . 14 |- ((a ~< om /\ b ~< om) -> (a X. b) ~< om)
190		simp3l3 983	. . . . . . . . . . . . . . . 16 |- (((a X. b) ~< om /\ -. b = (/) /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T)) -> T e. Tarski )
191	140	3ad2ant3 899	. . . . . . . . . . . . . . . . 17 |- (((a X. b) ~< om /\ -. b = (/) /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T)) -> a C_ T)
192	146	3ad2ant3 899	. . . . . . . . . . . . . . . . 17 |- (((a X. b) ~< om /\ -. b = (/) /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T)) -> b C_ T)
193	190, 191, 192, 30	syl111anc 1100	. . . . . . . . . . . . . . . 16 |- (((a X. b) ~< om /\ -. b = (/) /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T)) -> (a X. b) C_ T)
194		tclinf 15241	. . . . . . . . . . . . . . . . . . . . . 22 |- ((T e. Tarski /\ T =/= (/)) -> om ~<_ T)
195		sdomdomtr 5532	. . . . . . . . . . . . . . . . . . . . . . 23 |- (T e. Tarski -> (((a X. b) ~< om /\ om ~<_ T) -> (a X. b) ~< T))
196	195	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 |- ((T e. Tarski /\ T =/= (/)) -> (((a X. b) ~< om /\ om ~<_ T) -> (a X. b) ~< T))
197	194, 196	mpan2d 766	. . . . . . . . . . . . . . . . . . . . 21 |- ((T e. Tarski /\ T =/= (/)) -> ((a X. b) ~< om -> (a X. b) ~< T))
198	197	ancoms 484	. . . . . . . . . . . . . . . . . . . 20 |- ((T =/= (/) /\ T e. Tarski ) -> ((a X. b) ~< om -> (a X. b) ~< T))
199	198	3adant2 895	. . . . . . . . . . . . . . . . . . 19 |- ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) -> ((a X. b) ~< om -> (a X. b) ~< T))
200	199	adantr 425	. . . . . . . . . . . . . . . . . 18 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> ((a X. b) ~< om -> (a X. b) ~< T))
201	200	impcom 378	. . . . . . . . . . . . . . . . 17 |- (((a X. b) ~< om /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T)) -> (a X. b) ~< T)
202	201	3adant2 895	. . . . . . . . . . . . . . . 16 |- (((a X. b) ~< om /\ -. b = (/) /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T)) -> (a X. b) ~< T)
203	190, 193, 202, 33	syl111anc 1100	. . . . . . . . . . . . . . 15 |- (((a X. b) ~< om /\ -. b = (/) /\ ((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T)) -> (a X. b) e. T)
204	203	3exp 1066	. . . . . . . . . . . . . 14 |- ((a X. b) ~< om -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T)))
205	189, 204	syl 12	. . . . . . . . . . . . 13 |- ((a ~< om /\ b ~< om) -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T)))
206	205	expcom 403	. . . . . . . . . . . 12 |- (b ~< om -> (a ~< om -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))))
207	188, 206	sylbi 216	. . . . . . . . . . 11 |- (-. om ~<_ b -> (a ~< om -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))))
208	186, 207	pm2.61i 140	. . . . . . . . . 10 |- (a ~< om -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T)))
209	133, 208	sylbi 216	. . . . . . . . 9 |- (-. om ~<_ a -> (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T)))
210	130, 209	pm2.61i 140	. . . . . . . 8 |- (-. b = (/) -> (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T))
211	21, 210	pm2.61i 140	. . . . . . 7 |- (((T =/= (/) /\ (a e. T /\ b e. T) /\ T e. Tarski ) /\ Tr T) -> (a X. b) e. T)
212	211	3exp1 1084	. . . . . 6 |- (T =/= (/) -> ((a e. T /\ b e. T) -> (T e. Tarski -> (Tr T -> (a X. b) e. T))))
213	9, 212	syl 12	. . . . 5 |- (a e. T -> ((a e. T /\ b e. T) -> (T e. Tarski -> (Tr T -> (a X. b) e. T))))
214	213	anabsi5 553	. . . 4 |- ((a e. T /\ b e. T) -> (T e. Tarski -> (Tr T -> (a X. b) e. T)))
215	4, 8, 214	vtocl2ga 2353	. . 3 |- ((A e. T /\ B e. T) -> (T e. Tarski -> (Tr T -> (A X. B) e. T)))
216	215	com3l 38	. 2 |- (T e. Tarski -> (Tr T -> ((A e. T /\ B e. T) -> (A X. B) e. T)))
217	216	3imp 1061	1 |- ((T e. Tarski /\ Tr T /\ (A e. T /\ B e. T)) -> (A X. B) e. T)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  _Vcvv 2292   C_ wss 2593  (/)c0 2875   class class class wbr 3338  Tr wtr 3411  omcom 3949   X. cxp 3984   ~~ cen 5423   ~<_ cdom 5424   ~< csdm 5425   Tarski ctarski 15208

This theorem is referenced by:  sexptrt 15243

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-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695  ax-inf2 5731  ax-ac 5906

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  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-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  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-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-iso 4015  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-2o 5178  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-map 5383  df-en 5427  df-dom 5428  df-sdom 5429  df-fin 5430  df-undef 5556  df-riota 5560  df-card 5862  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-n 7108  df-2 7154  df-n0 7309  df-z 7345  df-seq1 7721  df-exp 7812  df-tsk 15210

Copyright terms: Public domain