Theorem elomsubsdOLD 15394

Description: If an ordinal is smaller than an initial ordinal, it is strictly dominated by it. (Moved to elomsubsd 5885 in main set.mm and may be deleted by mathbox owner, JGH. --NM 26-Aug-2011.)

Assertion

Ref	Expression
elomsubsdOLD	|- ((A e. On /\ B e. On) -> (A e. (aleph` B) <-> A ~< (aleph` B)))

Proof of Theorem elomsubsdOLD

Step	Hyp	Ref	Expression
1		fveq2 4681	. . . . . . 7 |- (k = (/) -> (aleph` k) = (aleph` (/)))
2	1	eleq2d 1964	. . . . . 6 |- (k = (/) -> (A e. (aleph` k) <-> A e. (aleph` (/))))
3	1	breq2d 3350	. . . . . 6 |- (k = (/) -> (A ~< (aleph` k) <-> A ~< (aleph` (/))))
4	2, 3	imbi12d 688	. . . . 5 |- (k = (/) -> ((A e. (aleph` k) -> A ~< (aleph` k)) <-> (A e. (aleph` (/)) -> A ~< (aleph` (/)))))
5	4	imbi2d 674	. . . 4 |- (k = (/) -> ((A e. On -> (A e. (aleph` k) -> A ~< (aleph` k))) <-> (A e. On -> (A e. (aleph` (/)) -> A ~< (aleph` (/))))))
6		fveq2 4681	. . . . . . 7 |- (k = j -> (aleph` k) = (aleph` j))
7	6	eleq2d 1964	. . . . . 6 |- (k = j -> (A e. (aleph` k) <-> A e. (aleph` j)))
8	6	breq2d 3350	. . . . . 6 |- (k = j -> (A ~< (aleph` k) <-> A ~< (aleph` j)))
9	7, 8	imbi12d 688	. . . . 5 |- (k = j -> ((A e. (aleph` k) -> A ~< (aleph` k)) <-> (A e. (aleph` j) -> A ~< (aleph` j))))
10	9	imbi2d 674	. . . 4 |- (k = j -> ((A e. On -> (A e. (aleph` k) -> A ~< (aleph` k))) <-> (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j)))))
11		fveq2 4681	. . . . . . 7 |- (k = suc j -> (aleph` k) = (aleph` suc j))
12	11	eleq2d 1964	. . . . . 6 |- (k = suc j -> (A e. (aleph` k) <-> A e. (aleph` suc j)))
13	11	breq2d 3350	. . . . . 6 |- (k = suc j -> (A ~< (aleph` k) <-> A ~< (aleph` suc j)))
14	12, 13	imbi12d 688	. . . . 5 |- (k = suc j -> ((A e. (aleph` k) -> A ~< (aleph` k)) <-> (A e. (aleph` suc j) -> A ~< (aleph` suc j))))
15	14	imbi2d 674	. . . 4 |- (k = suc j -> ((A e. On -> (A e. (aleph` k) -> A ~< (aleph` k))) <-> (A e. On -> (A e. (aleph` suc j) -> A ~< (aleph` suc j)))))
16		fveq2 4681	. . . . . . 7 |- (k = B -> (aleph` k) = (aleph` B))
17	16	eleq2d 1964	. . . . . 6 |- (k = B -> (A e. (aleph` k) <-> A e. (aleph` B)))
18	16	breq2d 3350	. . . . . 6 |- (k = B -> (A ~< (aleph` k) <-> A ~< (aleph` B)))
19	17, 18	imbi12d 688	. . . . 5 |- (k = B -> ((A e. (aleph` k) -> A ~< (aleph` k)) <-> (A e. (aleph` B) -> A ~< (aleph` B))))
20	19	imbi2d 674	. . . 4 |- (k = B -> ((A e. On -> (A e. (aleph` k) -> A ~< (aleph` k))) <-> (A e. On -> (A e. (aleph` B) -> A ~< (aleph` B)))))
21		nnsdom 5742	. . . . . 6 |- (A e. om -> A ~< om)
22		aleph0 5874	. . . . . . 7 |- (aleph` (/)) = om
23	22	eleq2i 1961	. . . . . 6 |- (A e. (aleph` (/)) <-> A e. om)
24	22	breq2i 3346	. . . . . 6 |- (A ~< (aleph` (/)) <-> A ~< om)
25	21, 23, 24	3imtr4i 236	. . . . 5 |- (A e. (aleph` (/)) -> A ~< (aleph` (/)))
26	25	a1i 8	. . . 4 |- (A e. On -> (A e. (aleph` (/)) -> A ~< (aleph` (/))))
27		brsdom 5440	. . . . . . . . 9 |- (A ~< |^|{x e. On | (aleph` j) ~< x} <-> (A ~<_ |^|{x e. On | (aleph` j) ~< x} /\ -. A ~~ |^|{x e. On | (aleph` j) ~< x}))
28		simplr 449	. . . . . . . . . 10 |- (((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) -> A e. On)
29		alephon 5876	. . . . . . . . . . . . . 14 |- (aleph` j) e. On
30		onsdom 5694	. . . . . . . . . . . . . 14 |- ((aleph` j) e. On -> E.x e. On (aleph` j) ~< x)
31	29, 30	ax-mp 7	. . . . . . . . . . . . 13 |- E.x e. On (aleph` j) ~< x
32		onintrab2 3883	. . . . . . . . . . . . 13 |- (E.x e. On (aleph` j) ~< x <-> |^|{x e. On | (aleph` j) ~< x} e. On)
33	31, 32	mpbi 206	. . . . . . . . . . . 12 |- |^|{x e. On | (aleph` j) ~< x} e. On
34		onelss 3705	. . . . . . . . . . . 12 |- (|^|{x e. On | (aleph` j) ~< x} e. On -> (A e. |^|{x e. On | (aleph` j) ~< x} -> A C_ |^|{x e. On | (aleph` j) ~< x}))
35	33, 34	ax-mp 7	. . . . . . . . . . 11 |- (A e. |^|{x e. On | (aleph` j) ~< x} -> A C_ |^|{x e. On | (aleph` j) ~< x})
36	35	adantl 424	. . . . . . . . . 10 |- (((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) -> A C_ |^|{x e. On | (aleph` j) ~< x})
37		ssdomg 5467	. . . . . . . . . 10 |- (A e. On -> (A C_ |^|{x e. On | (aleph` j) ~< x} -> A ~<_ |^|{x e. On | (aleph` j) ~< x}))
38	28, 36, 37	sylc 83	. . . . . . . . 9 |- (((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) -> A ~<_ |^|{x e. On | (aleph` j) ~< x})
39		eloni 3667	. . . . . . . . . . . . . 14 |- (A e. On -> Ord A)
40		eloni 3667	. . . . . . . . . . . . . . . 16 |- (|^|{x e. On | (aleph` j) ~< x} e. On -> Ord |^|{x e. On | (aleph` j) ~< x})
41	33, 40	ax-mp 7	. . . . . . . . . . . . . . 15 |- Ord |^|{x e. On | (aleph` j) ~< x}
42		ordtri1 3693	. . . . . . . . . . . . . . 15 |- ((Ord |^|{x e. On | (aleph` j) ~< x} /\ Ord A) -> (|^|{x e. On | (aleph` j) ~< x} C_ A <-> -. A e. |^|{x e. On | (aleph` j) ~< x}))
43	41, 42	mpan 759	. . . . . . . . . . . . . 14 |- (Ord A -> (|^|{x e. On | (aleph` j) ~< x} C_ A <-> -. A e. |^|{x e. On | (aleph` j) ~< x}))
44	39, 43	syl 12	. . . . . . . . . . . . 13 |- (A e. On -> (|^|{x e. On | (aleph` j) ~< x} C_ A <-> -. A e. |^|{x e. On | (aleph` j) ~< x}))
45	44	adantl 424	. . . . . . . . . . . 12 |- ((j e. On /\ A e. On) -> (|^|{x e. On | (aleph` j) ~< x} C_ A <-> -. A e. |^|{x e. On | (aleph` j) ~< x}))
46	45	con2bid 585	. . . . . . . . . . 11 |- ((j e. On /\ A e. On) -> (A e. |^|{x e. On | (aleph` j) ~< x} <-> -. |^|{x e. On | (aleph` j) ~< x} C_ A))
47	46	biimpa 460	. . . . . . . . . 10 |- (((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) -> -. |^|{x e. On | (aleph` j) ~< x} C_ A)
48	28	a1d 15	. . . . . . . . . . . . 13 |- (((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) -> (A ~~ |^|{x e. On | (aleph` j) ~< x} -> A e. On))
49		simpllr 453	. . . . . . . . . . . . . . 15 |- ((((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) /\ A ~~ |^|{x e. On | (aleph` j) ~< x}) -> A e. On)
50	33	a1i 8	. . . . . . . . . . . . . . . . 17 |- ((((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) /\ A ~~ |^|{x e. On | (aleph` j) ~< x}) -> |^|{x e. On | (aleph` j) ~< x} e. On)
51		simpr 350	. . . . . . . . . . . . . . . . 17 |- ((((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) /\ A ~~ |^|{x e. On | (aleph` j) ~< x}) -> A ~~ |^|{x e. On | (aleph` j) ~< x})
52		ensymg 5470	. . . . . . . . . . . . . . . . 17 |- (|^|{x e. On | (aleph` j) ~< x} e. On -> (A ~~ |^|{x e. On | (aleph` j) ~< x} -> |^|{x e. On | (aleph` j) ~< x} ~~ A))
53	50, 51, 52	sylc 83	. . . . . . . . . . . . . . . 16 |- ((((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) /\ A ~~ |^|{x e. On | (aleph` j) ~< x}) -> |^|{x e. On | (aleph` j) ~< x} ~~ A)
54		ax-17 1317	. . . . . . . . . . . . . . . . . . . 20 |- (y e. (aleph` j) -> A.x y e. (aleph` j))
55		ax-17 1317	. . . . . . . . . . . . . . . . . . . 20 |- (y e. ~< -> A.x y e. ~< )
56		hbrab1 2257	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. {x e. On | (aleph` j) ~< x} -> A.x y e. {x e. On | (aleph` j) ~< x})
57	56	hbint 3225	. . . . . . . . . . . . . . . . . . . 20 |- (y e. |^|{x e. On | (aleph` j) ~< x} -> A.x y e. |^|{x e. On | (aleph` j) ~< x})
58	54, 55, 57	hbbr 3381	. . . . . . . . . . . . . . . . . . 19 |- ((aleph` j) ~< |^|{x e. On | (aleph` j) ~< x} -> A.x(aleph` j) ~< |^|{x e. On | (aleph` j) ~< x})
59		breq2 3342	. . . . . . . . . . . . . . . . . . 19 |- (x = |^|{x e. On | (aleph` j) ~< x} -> ((aleph` j) ~< x <-> (aleph` j) ~< |^|{x e. On | (aleph` j) ~< x}))
60	58, 59	onminsb 3879	. . . . . . . . . . . . . . . . . 18 |- (E.x e. On (aleph` j) ~< x -> (aleph` j) ~< |^|{x e. On | (aleph` j) ~< x})
61	30, 60	syl 12	. . . . . . . . . . . . . . . . 17 |- ((aleph` j) e. On -> (aleph` j) ~< |^|{x e. On | (aleph` j) ~< x})
62	29, 61	ax-mp 7	. . . . . . . . . . . . . . . 16 |- (aleph` j) ~< |^|{x e. On | (aleph` j) ~< x}
63	53, 62	jctil 316	. . . . . . . . . . . . . . 15 |- ((((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) /\ A ~~ |^|{x e. On | (aleph` j) ~< x}) -> ((aleph` j) ~< |^|{x e. On | (aleph` j) ~< x} /\ |^|{x e. On | (aleph` j) ~< x} ~~ A))
64		sdomentr 5533	. . . . . . . . . . . . . . 15 |- (A e. On -> (((aleph` j) ~< |^|{x e. On | (aleph` j) ~< x} /\ |^|{x e. On | (aleph` j) ~< x} ~~ A) -> (aleph` j) ~< A))
65	49, 63, 64	sylc 83	. . . . . . . . . . . . . 14 |- ((((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) /\ A ~~ |^|{x e. On | (aleph` j) ~< x}) -> (aleph` j) ~< A)
66	65	ex 402	. . . . . . . . . . . . 13 |- (((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) -> (A ~~ |^|{x e. On | (aleph` j) ~< x} -> (aleph` j) ~< A))
67	48, 66	jcad 661	. . . . . . . . . . . 12 |- (((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) -> (A ~~ |^|{x e. On | (aleph` j) ~< x} -> (A e. On /\ (aleph` j) ~< A)))
68		breq2 3342	. . . . . . . . . . . . 13 |- (x = A -> ((aleph` j) ~< x <-> (aleph` j) ~< A))
69	68	elrab 2414	. . . . . . . . . . . 12 |- (A e. {x e. On | (aleph` j) ~< x} <-> (A e. On /\ (aleph` j) ~< A))
70	67, 69	syl6ibr 230	. . . . . . . . . . 11 |- (((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) -> (A ~~ |^|{x e. On | (aleph` j) ~< x} -> A e. {x e. On | (aleph` j) ~< x}))
71		intss1 3231	. . . . . . . . . . 11 |- (A e. {x e. On | (aleph` j) ~< x} -> |^|{x e. On | (aleph` j) ~< x} C_ A)
72	70, 71	syl6 25	. . . . . . . . . 10 |- (((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) -> (A ~~ |^|{x e. On | (aleph` j) ~< x} -> |^|{x e. On | (aleph` j) ~< x} C_ A))
73	47, 72	mtod 123	. . . . . . . . 9 |- (((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) -> -. A ~~ |^|{x e. On | (aleph` j) ~< x})
74	27, 38, 73	sylanbrc 527	. . . . . . . 8 |- (((j e. On /\ A e. On) /\ A e. |^|{x e. On | (aleph` j) ~< x}) -> A ~< |^|{x e. On | (aleph` j) ~< x})
75	74	ex 402	. . . . . . 7 |- ((j e. On /\ A e. On) -> (A e. |^|{x e. On | (aleph` j) ~< x} -> A ~< |^|{x e. On | (aleph` j) ~< x}))
76		omsubsuc 5877	. . . . . . . . 9 |- (j e. On -> (aleph` suc j) = |^|{x e. On | (aleph` j) ~< x})
77	76	eleq2d 1964	. . . . . . . 8 |- (j e. On -> (A e. (aleph` suc j) <-> A e. |^|{x e. On | (aleph` j) ~< x}))
78	77	adantr 425	. . . . . . 7 |- ((j e. On /\ A e. On) -> (A e. (aleph` suc j) <-> A e. |^|{x e. On | (aleph` j) ~< x}))
79	76	breq2d 3350	. . . . . . . 8 |- (j e. On -> (A ~< (aleph` suc j) <-> A ~< |^|{x e. On | (aleph` j) ~< x}))
80	79	adantr 425	. . . . . . 7 |- ((j e. On /\ A e. On) -> (A ~< (aleph` suc j) <-> A ~< |^|{x e. On | (aleph` j) ~< x}))
81	75, 78, 80	3imtr4d 602	. . . . . 6 |- ((j e. On /\ A e. On) -> (A e. (aleph` suc j) -> A ~< (aleph` suc j)))
82	81	ex 402	. . . . 5 |- (j e. On -> (A e. On -> (A e. (aleph` suc j) -> A ~< (aleph` suc j))))
83	82	a1d 15	. . . 4 |- (j e. On -> ((A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) -> (A e. On -> (A e. (aleph` suc j) -> A ~< (aleph` suc j)))))
84		hbra1 2147	. . . . . . . . . 10 |- (A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) -> A.jA.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))))
85		ax-17 1317	. . . . . . . . . 10 |- (A e. On -> A.j A e. On)
86	84, 85	hban 1356	. . . . . . . . 9 |- ((A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) /\ A e. On) -> A.j(A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) /\ A e. On))
87		ax-17 1317	. . . . . . . . . 10 |- (y e. A -> A.j y e. A)
88		ax-17 1317	. . . . . . . . . 10 |- (y e. ~< -> A.j y e. ~< )
89		hbiu1 3281	. . . . . . . . . 10 |- (y e. U_j e. k (aleph` j) -> A.j y e. U_j e. k (aleph` j))
90	87, 88, 89	hbbr 3381	. . . . . . . . 9 |- (A ~< U_j e. k (aleph` j) -> A.j A ~< U_j e. k (aleph` j))
91		ra4 2155	. . . . . . . . . . . . 13 |- (A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) -> (j e. k -> (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j)))))
92	91	com12 14	. . . . . . . . . . . 12 |- (j e. k -> (A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) -> (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j)))))
93		visset 2295	. . . . . . . . . . . . . . . . 17 |- k e. _V
94		fvex 4689	. . . . . . . . . . . . . . . . 17 |- (aleph` j) e. _V
95	93, 94	iunex 4839	. . . . . . . . . . . . . . . 16 |- U_j e. k (aleph` j) e. _V
96		sdomdomtr 5532	. . . . . . . . . . . . . . . 16 |- (U_j e. k (aleph` j) e. _V -> ((A ~< (aleph` j) /\ (aleph` j) ~<_ U_j e. k (aleph` j)) -> A ~< U_j e. k (aleph` j)))
97	95, 96	ax-mp 7	. . . . . . . . . . . . . . 15 |- ((A ~< (aleph` j) /\ (aleph` j) ~<_ U_j e. k (aleph` j)) -> A ~< U_j e. k (aleph` j))
98		ssiun2 3295	. . . . . . . . . . . . . . . 16 |- (j e. k -> (aleph` j) C_ U_j e. k (aleph` j))
99		ssdomg 5467	. . . . . . . . . . . . . . . . 17 |- ((aleph` j) e. _V -> ((aleph` j) C_ U_j e. k (aleph` j) -> (aleph` j) ~<_ U_j e. k (aleph` j)))
100	94, 99	ax-mp 7	. . . . . . . . . . . . . . . 16 |- ((aleph` j) C_ U_j e. k (aleph` j) -> (aleph` j) ~<_ U_j e. k (aleph` j))
101	98, 100	syl 12	. . . . . . . . . . . . . . 15 |- (j e. k -> (aleph` j) ~<_ U_j e. k (aleph` j))
102	97, 101	sylan2 500	. . . . . . . . . . . . . 14 |- ((A ~< (aleph` j) /\ j e. k) -> A ~< U_j e. k (aleph` j))
103	102	expcom 403	. . . . . . . . . . . . 13 |- (j e. k -> (A ~< (aleph` j) -> A ~< U_j e. k (aleph` j)))
104	103	imim2d 28	. . . . . . . . . . . 12 |- (j e. k -> ((A e. (aleph` j) -> A ~< (aleph` j)) -> (A e. (aleph` j) -> A ~< U_j e. k (aleph` j))))
105	92, 104	syl6d 67	. . . . . . . . . . 11 |- (j e. k -> (A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) -> (A e. On -> (A e. (aleph` j) -> A ~< U_j e. k (aleph` j)))))
106	105	imp3a 388	. . . . . . . . . 10 |- (j e. k -> ((A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) /\ A e. On) -> (A e. (aleph` j) -> A ~< U_j e. k (aleph` j))))
107	106	com12 14	. . . . . . . . 9 |- ((A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) /\ A e. On) -> (j e. k -> (A e. (aleph` j) -> A ~< U_j e. k (aleph` j))))
108	86, 90, 107	r19.23ad 2213	. . . . . . . 8 |- ((A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) /\ A e. On) -> (E.j e. k A e. (aleph` j) -> A ~< U_j e. k (aleph` j)))
109		eliun 3259	. . . . . . . 8 |- (A e. U_j e. k (aleph` j) <-> E.j e. k A e. (aleph` j))
110	108, 109	syl5ib 223	. . . . . . 7 |- ((A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) /\ A e. On) -> (A e. U_j e. k (aleph` j) -> A ~< U_j e. k (aleph` j)))
111	110	3adant1 894	. . . . . 6 |- ((Lim k /\ A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) /\ A e. On) -> (A e. U_j e. k (aleph` j) -> A ~< U_j e. k (aleph` j)))
112		alephlim 5875	. . . . . . . . 9 |- ((k e. _V /\ Lim k) -> (aleph` k) = U_j e. k (aleph` j))
113	93, 112	mpan 759	. . . . . . . 8 |- (Lim k -> (aleph` k) = U_j e. k (aleph` j))
114	113	eleq2d 1964	. . . . . . 7 |- (Lim k -> (A e. (aleph` k) <-> A e. U_j e. k (aleph` j)))
115	114	3ad2ant1 897	. . . . . 6 |- ((Lim k /\ A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) /\ A e. On) -> (A e. (aleph` k) <-> A e. U_j e. k (aleph` j)))
116	113	breq2d 3350	. . . . . . 7 |- (Lim k -> (A ~< (aleph` k) <-> A ~< U_j e. k (aleph` j)))
117	116	3ad2ant1 897	. . . . . 6 |- ((Lim k /\ A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) /\ A e. On) -> (A ~< (aleph` k) <-> A ~< U_j e. k (aleph` j)))
118	111, 115, 117	3imtr4d 602	. . . . 5 |- ((Lim k /\ A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) /\ A e. On) -> (A e. (aleph` k) -> A ~< (aleph` k)))
119	118	3exp 1066	. . . 4 |- (Lim k -> (A.j e. k (A e. On -> (A e. (aleph` j) -> A ~< (aleph` j))) -> (A e. On -> (A e. (aleph` k) -> A ~< (aleph` k)))))
120	5, 10, 15, 20, 26, 83, 119	tfinds 3942	. . 3 |- (B e. On -> (A e. On -> (A e. (aleph` B) -> A ~< (aleph` B))))
121	120	impcom 378	. 2 |- ((A e. On /\ B e. On) -> (A e. (aleph` B) -> A ~< (aleph` B)))
122		fvex 4689	. . . . 5 |- (aleph` B) e. _V
123		ssdomg 5467	. . . . 5 |- ((aleph` B) e. _V -> ((aleph` B) C_ A -> (aleph` B) ~<_ A))
124	122, 123	ax-mp 7	. . . 4 |- ((aleph` B) C_ A -> (aleph` B) ~<_ A)
125	124	a1i 8	. . 3 |- ((A e. On /\ B e. On) -> ((aleph` B) C_ A -> (aleph` B) ~<_ A))
126		alephon 5876	. . . . . . 7 |- (aleph` B) e. On
127		eloni 3667	. . . . . . 7 |- ((aleph` B) e. On -> Ord (aleph` B))
128	126, 127	ax-mp 7	. . . . . 6 |- Ord (aleph` B)
129		ordtri1 3693	. . . . . 6 |- ((Ord (aleph` B) /\ Ord A) -> ((aleph` B) C_ A <-> -. A e. (aleph` B)))
130	128, 129	mpan 759	. . . . 5 |- (Ord A -> ((aleph` B) C_ A <-> -. A e. (aleph` B)))
131	39, 130	syl 12	. . . 4 |- (A e. On -> ((aleph` B) C_ A <-> -. A e. (aleph` B)))
132	131	adantr 425	. . 3 |- ((A e. On /\ B e. On) -> ((aleph` B) C_ A <-> -. A e. (aleph` B)))
133		domtriord 5546	. . . . 5 |- (((aleph` B) e. On /\ A e. On) -> ((aleph` B) ~<_ A <-> -. A ~< (aleph` B)))
134	126, 133	mpan 759	. . . 4 |- (A e. On -> ((aleph` B) ~<_ A <-> -. A ~< (aleph` B)))
135	134	adantr 425	. . 3 |- ((A e. On /\ B e. On) -> ((aleph` B) ~<_ A <-> -. A ~< (aleph` B)))
136	125, 132, 135	3imtr3d 601	. 2 |- ((A e. On /\ B e. On) -> (-. A e. (aleph` B) -> -. A ~< (aleph` B)))
137	121, 136	impcon4bid 578	1 |- ((A e. On /\ B e. On) -> (A e. (aleph` B) <-> A ~< (aleph` B)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   C_ wss 2593  (/)c0 2875  |^|cint 3214  U_ciun 3255   class class class wbr 3338  Ord word 3656  Oncon0 3657  Lim wlim 3658  suc csuc 3659  omcom 3949  ` cfv 3998   ~~ cen 5423   ~<_ cdom 5424   ~< csdm 5425  alephcale 5860

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-inf2 5731

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-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-oprab 4887  df-rdg 5140  df-er 5318  df-en 5427  df-dom 5428  df-sdom 5429  df-fin 5430  df-aleph 5863

Copyright terms: Public domain