MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  omxpenlem Structured version   Visualization version   GIF version

Theorem omxpenlem 9024
Description: Lemma for omxpen 9025. (Contributed by Mario Carneiro, 3-Mar-2013.) (Revised by Mario Carneiro, 25-May-2015.)
Hypothesis
Ref Expression
omxpenlem.1 ๐น = (๐‘ฅ โˆˆ ๐ต, ๐‘ฆ โˆˆ ๐ด โ†ฆ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))
Assertion
Ref Expression
omxpenlem ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ๐น:(๐ต ร— ๐ด)โ€“1-1-ontoโ†’(๐ด ยทo ๐ต))
Distinct variable groups:   ๐‘ฅ,๐ด,๐‘ฆ   ๐‘ฅ,๐ต,๐‘ฆ
Allowed substitution hints:   ๐น(๐‘ฅ,๐‘ฆ)

Proof of Theorem omxpenlem
Dummy variables ๐‘š ๐‘› are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eloni 6332 . . . . . . . . 9 (๐ต โˆˆ On โ†’ Ord ๐ต)
21ad2antlr 726 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ Ord ๐ต)
3 simprl 770 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐‘ฅ โˆˆ ๐ต)
4 ordsucss 7758 . . . . . . . 8 (Ord ๐ต โ†’ (๐‘ฅ โˆˆ ๐ต โ†’ suc ๐‘ฅ โŠ† ๐ต))
52, 3, 4sylc 65 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ suc ๐‘ฅ โŠ† ๐ต)
6 onelon 6347 . . . . . . . . . 10 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ๐‘ฅ โˆˆ On)
76ad2ant2lr 747 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐‘ฅ โˆˆ On)
8 onsuc 7751 . . . . . . . . 9 (๐‘ฅ โˆˆ On โ†’ suc ๐‘ฅ โˆˆ On)
97, 8syl 17 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ suc ๐‘ฅ โˆˆ On)
10 simplr 768 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐ต โˆˆ On)
11 simpll 766 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐ด โˆˆ On)
12 omwordi 8523 . . . . . . . 8 ((suc ๐‘ฅ โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (suc ๐‘ฅ โŠ† ๐ต โ†’ (๐ด ยทo suc ๐‘ฅ) โŠ† (๐ด ยทo ๐ต)))
139, 10, 11, 12syl3anc 1372 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (suc ๐‘ฅ โŠ† ๐ต โ†’ (๐ด ยทo suc ๐‘ฅ) โŠ† (๐ด ยทo ๐ต)))
145, 13mpd 15 . . . . . 6 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐ด ยทo suc ๐‘ฅ) โŠ† (๐ด ยทo ๐ต))
15 simprr 772 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐‘ฆ โˆˆ ๐ด)
16 onelon 6347 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ ๐‘ฆ โˆˆ On)
1716ad2ant2rl 748 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐‘ฆ โˆˆ On)
18 omcl 8487 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
1911, 7, 18syl2anc 585 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
20 oaord 8499 . . . . . . . . 9 ((๐‘ฆ โˆˆ On โˆง ๐ด โˆˆ On โˆง (๐ด ยทo ๐‘ฅ) โˆˆ On) โ†’ (๐‘ฆ โˆˆ ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
2117, 11, 19, 20syl3anc 1372 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐‘ฆ โˆˆ ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
2215, 21mpbid 231 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด))
23 omsuc 8477 . . . . . . . 8 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo suc ๐‘ฅ) = ((๐ด ยทo ๐‘ฅ) +o ๐ด))
2411, 7, 23syl2anc 585 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐ด ยทo suc ๐‘ฅ) = ((๐ด ยทo ๐‘ฅ) +o ๐ด))
2522, 24eleqtrrd 2841 . . . . . 6 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo suc ๐‘ฅ))
2614, 25sseldd 3950 . . . . 5 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต))
2726ralrimivva 3198 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต))
28 omxpenlem.1 . . . . 5 ๐น = (๐‘ฅ โˆˆ ๐ต, ๐‘ฆ โˆˆ ๐ด โ†ฆ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))
2928fmpo 8005 . . . 4 (โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โ†” ๐น:(๐ต ร— ๐ด)โŸถ(๐ด ยทo ๐ต))
3027, 29sylib 217 . . 3 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ๐น:(๐ต ร— ๐ด)โŸถ(๐ด ยทo ๐ต))
3130ffnd 6674 . 2 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ๐น Fn (๐ต ร— ๐ด))
32 simpll 766 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ๐ด โˆˆ On)
33 omcl 8487 . . . . . . . 8 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ On)
34 onelon 6347 . . . . . . . 8 (((๐ด ยทo ๐ต) โˆˆ On โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ๐‘š โˆˆ On)
3533, 34sylan 581 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ๐‘š โˆˆ On)
36 noel 4295 . . . . . . . . . . . 12 ยฌ ๐‘š โˆˆ โˆ…
37 oveq1 7369 . . . . . . . . . . . . . 14 (๐ด = โˆ… โ†’ (๐ด ยทo ๐ต) = (โˆ… ยทo ๐ต))
38 om0r 8490 . . . . . . . . . . . . . 14 (๐ต โˆˆ On โ†’ (โˆ… ยทo ๐ต) = โˆ…)
3937, 38sylan9eqr 2799 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง ๐ด = โˆ…) โ†’ (๐ด ยทo ๐ต) = โˆ…)
4039eleq2d 2824 . . . . . . . . . . . 12 ((๐ต โˆˆ On โˆง ๐ด = โˆ…) โ†’ (๐‘š โˆˆ (๐ด ยทo ๐ต) โ†” ๐‘š โˆˆ โˆ…))
4136, 40mtbiri 327 . . . . . . . . . . 11 ((๐ต โˆˆ On โˆง ๐ด = โˆ…) โ†’ ยฌ ๐‘š โˆˆ (๐ด ยทo ๐ต))
4241ex 414 . . . . . . . . . 10 (๐ต โˆˆ On โ†’ (๐ด = โˆ… โ†’ ยฌ ๐‘š โˆˆ (๐ด ยทo ๐ต)))
4342necon2ad 2959 . . . . . . . . 9 (๐ต โˆˆ On โ†’ (๐‘š โˆˆ (๐ด ยทo ๐ต) โ†’ ๐ด โ‰  โˆ…))
4443adantl 483 . . . . . . . 8 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐‘š โˆˆ (๐ด ยทo ๐ต) โ†’ ๐ด โ‰  โˆ…))
4544imp 408 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ๐ด โ‰  โˆ…)
46 omeu 8537 . . . . . . 7 ((๐ด โˆˆ On โˆง ๐‘š โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆƒ!๐‘›โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))
4732, 35, 45, 46syl3anc 1372 . . . . . 6 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ โˆƒ!๐‘›โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))
48 vex 3452 . . . . . . . . 9 ๐‘š โˆˆ V
49 vex 3452 . . . . . . . . 9 ๐‘› โˆˆ V
5048, 49brcnv 5843 . . . . . . . 8 (๐‘šโ—ก๐น๐‘› โ†” ๐‘›๐น๐‘š)
51 eleq1 2826 . . . . . . . . . . . . . . . . 17 (๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โ†’ (๐‘š โˆˆ (๐ด ยทo ๐ต) โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)))
5251biimpac 480 . . . . . . . . . . . . . . . 16 ((๐‘š โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต))
536ex 414 . . . . . . . . . . . . . . . . . . . 20 (๐ต โˆˆ On โ†’ (๐‘ฅ โˆˆ ๐ต โ†’ ๐‘ฅ โˆˆ On))
5453ad2antlr 726 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐‘ฅ โˆˆ ๐ต โ†’ ๐‘ฅ โˆˆ On))
55 simplll 774 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐ด โˆˆ On)
56 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฅ โˆˆ On)
5755, 56, 18syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
58 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฆ โˆˆ ๐ด)
5955, 58, 16syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฆ โˆˆ On)
60 oaword1 8504 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐ด ยทo ๐‘ฅ) โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))
6157, 59, 60syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))
62 simplrl 776 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต))
6333ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ On)
64 ontr2 6369 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐ด ยทo ๐‘ฅ) โˆˆ On โˆง (๐ด ยทo ๐ต) โˆˆ On) โ†’ (((๐ด ยทo ๐‘ฅ) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต)))
6557, 63, 64syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (((๐ด ยทo ๐‘ฅ) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต)))
6661, 62, 65mp2and 698 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต))
67 simpllr 775 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐ต โˆˆ On)
6862ne0d 4300 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐ต) โ‰  โˆ…)
69 on0eln0 6378 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐ด ยทo ๐ต) โˆˆ On โ†’ (โˆ… โˆˆ (๐ด ยทo ๐ต) โ†” (๐ด ยทo ๐ต) โ‰  โˆ…))
7063, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆ… โˆˆ (๐ด ยทo ๐ต) โ†” (๐ด ยทo ๐ต) โ‰  โˆ…))
7168, 70mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ โˆ… โˆˆ (๐ด ยทo ๐ต))
72 om00el 8528 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (โˆ… โˆˆ (๐ด ยทo ๐ต) โ†” (โˆ… โˆˆ ๐ด โˆง โˆ… โˆˆ ๐ต)))
7372ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆ… โˆˆ (๐ด ยทo ๐ต) โ†” (โˆ… โˆˆ ๐ด โˆง โˆ… โˆˆ ๐ต)))
7471, 73mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆ… โˆˆ ๐ด โˆง โˆ… โˆˆ ๐ต))
7574simpld 496 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ โˆ… โˆˆ ๐ด)
76 omord2 8519 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ฅ โˆˆ ๐ต โ†” (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต)))
7756, 67, 55, 75, 76syl31anc 1374 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐‘ฅ โˆˆ ๐ต โ†” (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต)))
7866, 77mpbird 257 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฅ โˆˆ ๐ต)
7978ex 414 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐‘ฅ โˆˆ On โ†’ ๐‘ฅ โˆˆ ๐ต))
8054, 79impbid 211 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐‘ฅ โˆˆ ๐ต โ†” ๐‘ฅ โˆˆ On))
8180expr 458 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐‘ฆ โˆˆ ๐ด โ†’ (๐‘ฅ โˆˆ ๐ต โ†” ๐‘ฅ โˆˆ On)))
8281pm5.32rd 579 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)) โ†’ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โ†” (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด)))
8352, 82sylan2 594 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘š โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))) โ†’ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โ†” (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด)))
8483expr 458 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โ†’ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โ†” (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด))))
8584pm5.32rd 579 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))))
86 eqcom 2744 . . . . . . . . . . . . . 14 (๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)
8786anbi2i 624 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))
8885, 87bitrdi 287 . . . . . . . . . . . 12 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
8988anbi2d 630 . . . . . . . . . . 11 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ((๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))) โ†” (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))))
90 an12 644 . . . . . . . . . . 11 ((๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
9189, 90bitrdi 287 . . . . . . . . . 10 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ((๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))))
92912exbidv 1928 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))) โ†” โˆƒ๐‘ฅโˆƒ๐‘ฆ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))))
93 df-mpo 7367 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ ๐ต, ๐‘ฆ โˆˆ ๐ด โ†ฆ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) = {โŸจโŸจ๐‘ฅ, ๐‘ฆโŸฉ, ๐‘šโŸฉ โˆฃ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))}
94 dfoprab2 7420 . . . . . . . . . . . 12 {โŸจโŸจ๐‘ฅ, ๐‘ฆโŸฉ, ๐‘šโŸฉ โˆฃ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))} = {โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))}
9528, 93, 943eqtri 2769 . . . . . . . . . . 11 ๐น = {โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))}
9695breqi 5116 . . . . . . . . . 10 (๐‘›๐น๐‘š โ†” ๐‘›{โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))}๐‘š)
97 df-br 5111 . . . . . . . . . 10 (๐‘›{โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))}๐‘š โ†” โŸจ๐‘›, ๐‘šโŸฉ โˆˆ {โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))})
98 opabidw 5486 . . . . . . . . . 10 (โŸจ๐‘›, ๐‘šโŸฉ โˆˆ {โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))} โ†” โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))))
9996, 97, 983bitri 297 . . . . . . . . 9 (๐‘›๐น๐‘š โ†” โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))))
100 r2ex 3193 . . . . . . . . 9 (โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š) โ†” โˆƒ๐‘ฅโˆƒ๐‘ฆ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
10192, 99, 1003bitr4g 314 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐‘›๐น๐‘š โ†” โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
10250, 101bitrid 283 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐‘šโ—ก๐น๐‘› โ†” โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
103102eubidv 2585 . . . . . 6 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (โˆƒ!๐‘› ๐‘šโ—ก๐น๐‘› โ†” โˆƒ!๐‘›โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
10447, 103mpbird 257 . . . . 5 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ โˆƒ!๐‘› ๐‘šโ—ก๐น๐‘›)
105104ralrimiva 3144 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ โˆ€๐‘š โˆˆ (๐ด ยทo ๐ต)โˆƒ!๐‘› ๐‘šโ—ก๐น๐‘›)
106 fnres 6633 . . . 4 ((โ—ก๐น โ†พ (๐ด ยทo ๐ต)) Fn (๐ด ยทo ๐ต) โ†” โˆ€๐‘š โˆˆ (๐ด ยทo ๐ต)โˆƒ!๐‘› ๐‘šโ—ก๐น๐‘›)
107105, 106sylibr 233 . . 3 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (โ—ก๐น โ†พ (๐ด ยทo ๐ต)) Fn (๐ด ยทo ๐ต))
108 relcnv 6061 . . . . 5 Rel โ—ก๐น
109 df-rn 5649 . . . . . 6 ran ๐น = dom โ—ก๐น
11030frnd 6681 . . . . . 6 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ran ๐น โŠ† (๐ด ยทo ๐ต))
111109, 110eqsstrrid 3998 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ dom โ—ก๐น โŠ† (๐ด ยทo ๐ต))
112 relssres 5983 . . . . 5 ((Rel โ—ก๐น โˆง dom โ—ก๐น โŠ† (๐ด ยทo ๐ต)) โ†’ (โ—ก๐น โ†พ (๐ด ยทo ๐ต)) = โ—ก๐น)
113108, 111, 112sylancr 588 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (โ—ก๐น โ†พ (๐ด ยทo ๐ต)) = โ—ก๐น)
114113fneq1d 6600 . . 3 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((โ—ก๐น โ†พ (๐ด ยทo ๐ต)) Fn (๐ด ยทo ๐ต) โ†” โ—ก๐น Fn (๐ด ยทo ๐ต)))
115107, 114mpbid 231 . 2 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ โ—ก๐น Fn (๐ด ยทo ๐ต))
116 dff1o4 6797 . 2 (๐น:(๐ต ร— ๐ด)โ€“1-1-ontoโ†’(๐ด ยทo ๐ต) โ†” (๐น Fn (๐ต ร— ๐ด) โˆง โ—ก๐น Fn (๐ด ยทo ๐ต)))
11731, 115, 116sylanbrc 584 1 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ๐น:(๐ต ร— ๐ด)โ€“1-1-ontoโ†’(๐ด ยทo ๐ต))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542  โˆƒwex 1782   โˆˆ wcel 2107  โˆƒ!weu 2567   โ‰  wne 2944  โˆ€wral 3065  โˆƒwrex 3074   โŠ† wss 3915  โˆ…c0 4287  โŸจcop 4597   class class class wbr 5110  {copab 5172   ร— cxp 5636  โ—กccnv 5637  dom cdm 5638  ran crn 5639   โ†พ cres 5640  Rel wrel 5643  Ord word 6321  Oncon0 6322  suc csuc 6324   Fn wfn 6496  โŸถwf 6497  โ€“1-1-ontoโ†’wf1o 6500  (class class class)co 7362  {coprab 7363   โˆˆ cmpo 7364   +o coa 8414   ยทo comu 8415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-oadd 8421  df-omul 8422
This theorem is referenced by:  omxpen  9025  omf1o  9026  infxpenc  9961
  Copyright terms: Public domain W3C validator