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

Theorem omxpenlem 9075
Description: Lemma for omxpen 9076. (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 6373 . . . . . . . . 9 (๐ต โˆˆ On โ†’ Ord ๐ต)
21ad2antlr 723 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ Ord ๐ต)
3 simprl 767 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐‘ฅ โˆˆ ๐ต)
4 ordsucss 7808 . . . . . . . 8 (Ord ๐ต โ†’ (๐‘ฅ โˆˆ ๐ต โ†’ suc ๐‘ฅ โІ ๐ต))
52, 3, 4sylc 65 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ suc ๐‘ฅ โІ ๐ต)
6 onelon 6388 . . . . . . . . . 10 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ๐‘ฅ โˆˆ On)
76ad2ant2lr 744 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐‘ฅ โˆˆ On)
8 onsuc 7801 . . . . . . . . 9 (๐‘ฅ โˆˆ On โ†’ suc ๐‘ฅ โˆˆ On)
97, 8syl 17 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ suc ๐‘ฅ โˆˆ On)
10 simplr 765 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐ต โˆˆ On)
11 simpll 763 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐ด โˆˆ On)
12 omwordi 8573 . . . . . . . 8 ((suc ๐‘ฅ โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (suc ๐‘ฅ โІ ๐ต โ†’ (๐ด ยทo suc ๐‘ฅ) โІ (๐ด ยทo ๐ต)))
139, 10, 11, 12syl3anc 1369 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (suc ๐‘ฅ โІ ๐ต โ†’ (๐ด ยทo suc ๐‘ฅ) โІ (๐ด ยทo ๐ต)))
145, 13mpd 15 . . . . . 6 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐ด ยทo suc ๐‘ฅ) โІ (๐ด ยทo ๐ต))
15 simprr 769 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐‘ฆ โˆˆ ๐ด)
16 onelon 6388 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ ๐‘ฆ โˆˆ On)
1716ad2ant2rl 745 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐‘ฆ โˆˆ On)
18 omcl 8538 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
1911, 7, 18syl2anc 582 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
20 oaord 8549 . . . . . . . . 9 ((๐‘ฆ โˆˆ On โˆง ๐ด โˆˆ On โˆง (๐ด ยทo ๐‘ฅ) โˆˆ On) โ†’ (๐‘ฆ โˆˆ ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
2117, 11, 19, 20syl3anc 1369 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐‘ฆ โˆˆ ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
2215, 21mpbid 231 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด))
23 omsuc 8528 . . . . . . . 8 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo suc ๐‘ฅ) = ((๐ด ยทo ๐‘ฅ) +o ๐ด))
2411, 7, 23syl2anc 582 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐ด ยทo suc ๐‘ฅ) = ((๐ด ยทo ๐‘ฅ) +o ๐ด))
2522, 24eleqtrrd 2834 . . . . . 6 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo suc ๐‘ฅ))
2614, 25sseldd 3982 . . . . 5 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต))
2726ralrimivva 3198 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต))
28 omxpenlem.1 . . . . 5 ๐น = (๐‘ฅ โˆˆ ๐ต, ๐‘ฆ โˆˆ ๐ด โ†ฆ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))
2928fmpo 8056 . . . 4 (โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โ†” ๐น:(๐ต ร— ๐ด)โŸถ(๐ด ยทo ๐ต))
3027, 29sylib 217 . . 3 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ๐น:(๐ต ร— ๐ด)โŸถ(๐ด ยทo ๐ต))
3130ffnd 6717 . 2 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ๐น Fn (๐ต ร— ๐ด))
32 simpll 763 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ๐ด โˆˆ On)
33 omcl 8538 . . . . . . . 8 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ On)
34 onelon 6388 . . . . . . . 8 (((๐ด ยทo ๐ต) โˆˆ On โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ๐‘š โˆˆ On)
3533, 34sylan 578 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ๐‘š โˆˆ On)
36 noel 4329 . . . . . . . . . . . 12 ยฌ ๐‘š โˆˆ โˆ…
37 oveq1 7418 . . . . . . . . . . . . . 14 (๐ด = โˆ… โ†’ (๐ด ยทo ๐ต) = (โˆ… ยทo ๐ต))
38 om0r 8541 . . . . . . . . . . . . . 14 (๐ต โˆˆ On โ†’ (โˆ… ยทo ๐ต) = โˆ…)
3937, 38sylan9eqr 2792 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง ๐ด = โˆ…) โ†’ (๐ด ยทo ๐ต) = โˆ…)
4039eleq2d 2817 . . . . . . . . . . . 12 ((๐ต โˆˆ On โˆง ๐ด = โˆ…) โ†’ (๐‘š โˆˆ (๐ด ยทo ๐ต) โ†” ๐‘š โˆˆ โˆ…))
4136, 40mtbiri 326 . . . . . . . . . . 11 ((๐ต โˆˆ On โˆง ๐ด = โˆ…) โ†’ ยฌ ๐‘š โˆˆ (๐ด ยทo ๐ต))
4241ex 411 . . . . . . . . . 10 (๐ต โˆˆ On โ†’ (๐ด = โˆ… โ†’ ยฌ ๐‘š โˆˆ (๐ด ยทo ๐ต)))
4342necon2ad 2953 . . . . . . . . 9 (๐ต โˆˆ On โ†’ (๐‘š โˆˆ (๐ด ยทo ๐ต) โ†’ ๐ด โ‰  โˆ…))
4443adantl 480 . . . . . . . 8 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐‘š โˆˆ (๐ด ยทo ๐ต) โ†’ ๐ด โ‰  โˆ…))
4544imp 405 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ๐ด โ‰  โˆ…)
46 omeu 8587 . . . . . . 7 ((๐ด โˆˆ On โˆง ๐‘š โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆƒ!๐‘›โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))
4732, 35, 45, 46syl3anc 1369 . . . . . 6 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ โˆƒ!๐‘›โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))
48 vex 3476 . . . . . . . . 9 ๐‘š โˆˆ V
49 vex 3476 . . . . . . . . 9 ๐‘› โˆˆ V
5048, 49brcnv 5881 . . . . . . . 8 (๐‘šโ—ก๐น๐‘› โ†” ๐‘›๐น๐‘š)
51 eleq1 2819 . . . . . . . . . . . . . . . . 17 (๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โ†’ (๐‘š โˆˆ (๐ด ยทo ๐ต) โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)))
5251biimpac 477 . . . . . . . . . . . . . . . 16 ((๐‘š โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต))
536ex 411 . . . . . . . . . . . . . . . . . . . 20 (๐ต โˆˆ On โ†’ (๐‘ฅ โˆˆ ๐ต โ†’ ๐‘ฅ โˆˆ On))
5453ad2antlr 723 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐‘ฅ โˆˆ ๐ต โ†’ ๐‘ฅ โˆˆ On))
55 simplll 771 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐ด โˆˆ On)
56 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฅ โˆˆ On)
5755, 56, 18syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
58 simplrr 774 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฆ โˆˆ ๐ด)
5955, 58, 16syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฆ โˆˆ On)
60 oaword1 8554 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐ด ยทo ๐‘ฅ) โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โІ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))
6157, 59, 60syl2anc 582 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โІ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))
62 simplrl 773 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต))
6333ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ On)
64 ontr2 6410 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐ด ยทo ๐‘ฅ) โˆˆ On โˆง (๐ด ยทo ๐ต) โˆˆ On) โ†’ (((๐ด ยทo ๐‘ฅ) โІ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต)))
6557, 63, 64syl2anc 582 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (((๐ด ยทo ๐‘ฅ) โІ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต)))
6661, 62, 65mp2and 695 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต))
67 simpllr 772 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐ต โˆˆ On)
6862ne0d 4334 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐ต) โ‰  โˆ…)
69 on0eln0 6419 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐ด ยทo ๐ต) โˆˆ On โ†’ (โˆ… โˆˆ (๐ด ยทo ๐ต) โ†” (๐ด ยทo ๐ต) โ‰  โˆ…))
7063, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆ… โˆˆ (๐ด ยทo ๐ต) โ†” (๐ด ยทo ๐ต) โ‰  โˆ…))
7168, 70mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ โˆ… โˆˆ (๐ด ยทo ๐ต))
72 om00el 8578 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (โˆ… โˆˆ (๐ด ยทo ๐ต) โ†” (โˆ… โˆˆ ๐ด โˆง โˆ… โˆˆ ๐ต)))
7372ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆ… โˆˆ (๐ด ยทo ๐ต) โ†” (โˆ… โˆˆ ๐ด โˆง โˆ… โˆˆ ๐ต)))
7471, 73mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆ… โˆˆ ๐ด โˆง โˆ… โˆˆ ๐ต))
7574simpld 493 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ โˆ… โˆˆ ๐ด)
76 omord2 8569 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ฅ โˆˆ ๐ต โ†” (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต)))
7756, 67, 55, 75, 76syl31anc 1371 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐‘ฅ โˆˆ ๐ต โ†” (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต)))
7866, 77mpbird 256 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฅ โˆˆ ๐ต)
7978ex 411 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐‘ฅ โˆˆ On โ†’ ๐‘ฅ โˆˆ ๐ต))
8054, 79impbid 211 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐‘ฅ โˆˆ ๐ต โ†” ๐‘ฅ โˆˆ On))
8180expr 455 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐‘ฆ โˆˆ ๐ด โ†’ (๐‘ฅ โˆˆ ๐ต โ†” ๐‘ฅ โˆˆ On)))
8281pm5.32rd 576 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)) โ†’ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โ†” (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด)))
8352, 82sylan2 591 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘š โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))) โ†’ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โ†” (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด)))
8483expr 455 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โ†’ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โ†” (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด))))
8584pm5.32rd 576 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))))
86 eqcom 2737 . . . . . . . . . . . . . 14 (๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)
8786anbi2i 621 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))
8885, 87bitrdi 286 . . . . . . . . . . . 12 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
8988anbi2d 627 . . . . . . . . . . 11 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ((๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))) โ†” (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))))
90 an12 641 . . . . . . . . . . 11 ((๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
9189, 90bitrdi 286 . . . . . . . . . 10 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ((๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))))
92912exbidv 1925 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))) โ†” โˆƒ๐‘ฅโˆƒ๐‘ฆ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))))
93 df-mpo 7416 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ ๐ต, ๐‘ฆ โˆˆ ๐ด โ†ฆ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) = {โŸจโŸจ๐‘ฅ, ๐‘ฆโŸฉ, ๐‘šโŸฉ โˆฃ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))}
94 dfoprab2 7469 . . . . . . . . . . . 12 {โŸจโŸจ๐‘ฅ, ๐‘ฆโŸฉ, ๐‘šโŸฉ โˆฃ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))} = {โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))}
9528, 93, 943eqtri 2762 . . . . . . . . . . 11 ๐น = {โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))}
9695breqi 5153 . . . . . . . . . 10 (๐‘›๐น๐‘š โ†” ๐‘›{โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))}๐‘š)
97 df-br 5148 . . . . . . . . . 10 (๐‘›{โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))}๐‘š โ†” โŸจ๐‘›, ๐‘šโŸฉ โˆˆ {โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))})
98 opabidw 5523 . . . . . . . . . 10 (โŸจ๐‘›, ๐‘šโŸฉ โˆˆ {โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))} โ†” โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))))
9996, 97, 983bitri 296 . . . . . . . . 9 (๐‘›๐น๐‘š โ†” โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))))
100 r2ex 3193 . . . . . . . . 9 (โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š) โ†” โˆƒ๐‘ฅโˆƒ๐‘ฆ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
10192, 99, 1003bitr4g 313 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐‘›๐น๐‘š โ†” โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
10250, 101bitrid 282 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐‘šโ—ก๐น๐‘› โ†” โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
103102eubidv 2578 . . . . . 6 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (โˆƒ!๐‘› ๐‘šโ—ก๐น๐‘› โ†” โˆƒ!๐‘›โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
10447, 103mpbird 256 . . . . 5 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ โˆƒ!๐‘› ๐‘šโ—ก๐น๐‘›)
105104ralrimiva 3144 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ โˆ€๐‘š โˆˆ (๐ด ยทo ๐ต)โˆƒ!๐‘› ๐‘šโ—ก๐น๐‘›)
106 fnres 6676 . . . 4 ((โ—ก๐น โ†พ (๐ด ยทo ๐ต)) Fn (๐ด ยทo ๐ต) โ†” โˆ€๐‘š โˆˆ (๐ด ยทo ๐ต)โˆƒ!๐‘› ๐‘šโ—ก๐น๐‘›)
107105, 106sylibr 233 . . 3 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (โ—ก๐น โ†พ (๐ด ยทo ๐ต)) Fn (๐ด ยทo ๐ต))
108 relcnv 6102 . . . . 5 Rel โ—ก๐น
109 df-rn 5686 . . . . . 6 ran ๐น = dom โ—ก๐น
11030frnd 6724 . . . . . 6 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ran ๐น โІ (๐ด ยทo ๐ต))
111109, 110eqsstrrid 4030 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ dom โ—ก๐น โІ (๐ด ยทo ๐ต))
112 relssres 6021 . . . . 5 ((Rel โ—ก๐น โˆง dom โ—ก๐น โІ (๐ด ยทo ๐ต)) โ†’ (โ—ก๐น โ†พ (๐ด ยทo ๐ต)) = โ—ก๐น)
113108, 111, 112sylancr 585 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (โ—ก๐น โ†พ (๐ด ยทo ๐ต)) = โ—ก๐น)
114113fneq1d 6641 . . 3 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((โ—ก๐น โ†พ (๐ด ยทo ๐ต)) Fn (๐ด ยทo ๐ต) โ†” โ—ก๐น Fn (๐ด ยทo ๐ต)))
115107, 114mpbid 231 . 2 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ โ—ก๐น Fn (๐ด ยทo ๐ต))
116 dff1o4 6840 . 2 (๐น:(๐ต ร— ๐ด)โ€“1-1-ontoโ†’(๐ด ยทo ๐ต) โ†” (๐น Fn (๐ต ร— ๐ด) โˆง โ—ก๐น Fn (๐ด ยทo ๐ต)))
11731, 115, 116sylanbrc 581 1 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ๐น:(๐ต ร— ๐ด)โ€“1-1-ontoโ†’(๐ด ยทo ๐ต))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 394   = wceq 1539  โˆƒwex 1779   โˆˆ wcel 2104  โˆƒ!weu 2560   โ‰  wne 2938  โˆ€wral 3059  โˆƒwrex 3068   โІ wss 3947  โˆ…c0 4321  โŸจcop 4633   class class class wbr 5147  {copab 5209   ร— cxp 5673  โ—กccnv 5674  dom cdm 5675  ran crn 5676   โ†พ cres 5677  Rel wrel 5680  Ord word 6362  Oncon0 6363  suc csuc 6365   Fn wfn 6537  โŸถwf 6538  โ€“1-1-ontoโ†’wf1o 6541  (class class class)co 7411  {coprab 7412   โˆˆ cmpo 7413   +o coa 8465   ยทo comu 8466
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-omul 8473
This theorem is referenced by:  omxpen  9076  omf1o  9077  infxpenc  10015
  Copyright terms: Public domain W3C validator