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

Theorem omxpenlem 9077
Description: Lemma for omxpen 9078. (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 6374 . . . . . . . . 9 (๐ต โˆˆ On โ†’ Ord ๐ต)
21ad2antlr 724 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ Ord ๐ต)
3 simprl 768 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐‘ฅ โˆˆ ๐ต)
4 ordsucss 7810 . . . . . . . 8 (Ord ๐ต โ†’ (๐‘ฅ โˆˆ ๐ต โ†’ suc ๐‘ฅ โŠ† ๐ต))
52, 3, 4sylc 65 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ suc ๐‘ฅ โŠ† ๐ต)
6 onelon 6389 . . . . . . . . . 10 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ๐‘ฅ โˆˆ On)
76ad2ant2lr 745 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐‘ฅ โˆˆ On)
8 onsuc 7803 . . . . . . . . 9 (๐‘ฅ โˆˆ On โ†’ suc ๐‘ฅ โˆˆ On)
97, 8syl 17 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ suc ๐‘ฅ โˆˆ On)
10 simplr 766 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐ต โˆˆ On)
11 simpll 764 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐ด โˆˆ On)
12 omwordi 8575 . . . . . . . 8 ((suc ๐‘ฅ โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โˆˆ On) โ†’ (suc ๐‘ฅ โŠ† ๐ต โ†’ (๐ด ยทo suc ๐‘ฅ) โŠ† (๐ด ยทo ๐ต)))
139, 10, 11, 12syl3anc 1370 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (suc ๐‘ฅ โŠ† ๐ต โ†’ (๐ด ยทo suc ๐‘ฅ) โŠ† (๐ด ยทo ๐ต)))
145, 13mpd 15 . . . . . 6 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐ด ยทo suc ๐‘ฅ) โŠ† (๐ด ยทo ๐ต))
15 simprr 770 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐‘ฆ โˆˆ ๐ด)
16 onelon 6389 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ ๐‘ฆ โˆˆ On)
1716ad2ant2rl 746 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ๐‘ฆ โˆˆ On)
18 omcl 8540 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
1911, 7, 18syl2anc 583 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
20 oaord 8551 . . . . . . . . 9 ((๐‘ฆ โˆˆ On โˆง ๐ด โˆˆ On โˆง (๐ด ยทo ๐‘ฅ) โˆˆ On) โ†’ (๐‘ฆ โˆˆ ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
2117, 11, 19, 20syl3anc 1370 . . . . . . . 8 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐‘ฆ โˆˆ ๐ด โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด)))
2215, 21mpbid 231 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ ((๐ด ยทo ๐‘ฅ) +o ๐ด))
23 omsuc 8530 . . . . . . . 8 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo suc ๐‘ฅ) = ((๐ด ยทo ๐‘ฅ) +o ๐ด))
2411, 7, 23syl2anc 583 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐ด ยทo suc ๐‘ฅ) = ((๐ด ยทo ๐‘ฅ) +o ๐ด))
2522, 24eleqtrrd 2835 . . . . . 6 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo suc ๐‘ฅ))
2614, 25sseldd 3983 . . . . 5 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต))
2726ralrimivva 3199 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต))
28 omxpenlem.1 . . . . 5 ๐น = (๐‘ฅ โˆˆ ๐ต, ๐‘ฆ โˆˆ ๐ด โ†ฆ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))
2928fmpo 8058 . . . 4 (โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ด ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โ†” ๐น:(๐ต ร— ๐ด)โŸถ(๐ด ยทo ๐ต))
3027, 29sylib 217 . . 3 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ๐น:(๐ต ร— ๐ด)โŸถ(๐ด ยทo ๐ต))
3130ffnd 6718 . 2 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ๐น Fn (๐ต ร— ๐ด))
32 simpll 764 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ๐ด โˆˆ On)
33 omcl 8540 . . . . . . . 8 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ On)
34 onelon 6389 . . . . . . . 8 (((๐ด ยทo ๐ต) โˆˆ On โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ๐‘š โˆˆ On)
3533, 34sylan 579 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ๐‘š โˆˆ On)
36 noel 4330 . . . . . . . . . . . 12 ยฌ ๐‘š โˆˆ โˆ…
37 oveq1 7419 . . . . . . . . . . . . . 14 (๐ด = โˆ… โ†’ (๐ด ยทo ๐ต) = (โˆ… ยทo ๐ต))
38 om0r 8543 . . . . . . . . . . . . . 14 (๐ต โˆˆ On โ†’ (โˆ… ยทo ๐ต) = โˆ…)
3937, 38sylan9eqr 2793 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง ๐ด = โˆ…) โ†’ (๐ด ยทo ๐ต) = โˆ…)
4039eleq2d 2818 . . . . . . . . . . . 12 ((๐ต โˆˆ On โˆง ๐ด = โˆ…) โ†’ (๐‘š โˆˆ (๐ด ยทo ๐ต) โ†” ๐‘š โˆˆ โˆ…))
4136, 40mtbiri 327 . . . . . . . . . . 11 ((๐ต โˆˆ On โˆง ๐ด = โˆ…) โ†’ ยฌ ๐‘š โˆˆ (๐ด ยทo ๐ต))
4241ex 412 . . . . . . . . . 10 (๐ต โˆˆ On โ†’ (๐ด = โˆ… โ†’ ยฌ ๐‘š โˆˆ (๐ด ยทo ๐ต)))
4342necon2ad 2954 . . . . . . . . 9 (๐ต โˆˆ On โ†’ (๐‘š โˆˆ (๐ด ยทo ๐ต) โ†’ ๐ด โ‰  โˆ…))
4443adantl 481 . . . . . . . 8 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐‘š โˆˆ (๐ด ยทo ๐ต) โ†’ ๐ด โ‰  โˆ…))
4544imp 406 . . . . . . 7 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ๐ด โ‰  โˆ…)
46 omeu 8589 . . . . . . 7 ((๐ด โˆˆ On โˆง ๐‘š โˆˆ On โˆง ๐ด โ‰  โˆ…) โ†’ โˆƒ!๐‘›โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))
4732, 35, 45, 46syl3anc 1370 . . . . . 6 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ โˆƒ!๐‘›โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))
48 vex 3477 . . . . . . . . 9 ๐‘š โˆˆ V
49 vex 3477 . . . . . . . . 9 ๐‘› โˆˆ V
5048, 49brcnv 5882 . . . . . . . 8 (๐‘šโ—ก๐น๐‘› โ†” ๐‘›๐น๐‘š)
51 eleq1 2820 . . . . . . . . . . . . . . . . 17 (๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โ†’ (๐‘š โˆˆ (๐ด ยทo ๐ต) โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)))
5251biimpac 478 . . . . . . . . . . . . . . . 16 ((๐‘š โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต))
536ex 412 . . . . . . . . . . . . . . . . . . . 20 (๐ต โˆˆ On โ†’ (๐‘ฅ โˆˆ ๐ต โ†’ ๐‘ฅ โˆˆ On))
5453ad2antlr 724 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐‘ฅ โˆˆ ๐ต โ†’ ๐‘ฅ โˆˆ On))
55 simplll 772 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐ด โˆˆ On)
56 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฅ โˆˆ On)
5755, 56, 18syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ On)
58 simplrr 775 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฆ โˆˆ ๐ด)
5955, 58, 16syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฆ โˆˆ On)
60 oaword1 8556 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐ด ยทo ๐‘ฅ) โˆˆ On โˆง ๐‘ฆ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))
6157, 59, 60syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))
62 simplrl 774 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต))
6333ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐ต) โˆˆ On)
64 ontr2 6411 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐ด ยทo ๐‘ฅ) โˆˆ On โˆง (๐ด ยทo ๐ต) โˆˆ On) โ†’ (((๐ด ยทo ๐‘ฅ) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต)))
6557, 63, 64syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (((๐ด ยทo ๐‘ฅ) โŠ† ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต)))
6661, 62, 65mp2and 696 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต))
67 simpllr 773 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐ต โˆˆ On)
6862ne0d 4335 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด ยทo ๐ต) โ‰  โˆ…)
69 on0eln0 6420 . . . . . . . . . . . . . . . . . . . . . . . . . 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 8580 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (โˆ… โˆˆ (๐ด ยทo ๐ต) โ†” (โˆ… โˆˆ ๐ด โˆง โˆ… โˆˆ ๐ต)))
7372ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆ… โˆˆ (๐ด ยทo ๐ต) โ†” (โˆ… โˆˆ ๐ด โˆง โˆ… โˆˆ ๐ต)))
7471, 73mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (โˆ… โˆˆ ๐ด โˆง โˆ… โˆˆ ๐ต))
7574simpld 494 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ โˆ… โˆˆ ๐ด)
76 omord2 8571 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โˆˆ On) โˆง โˆ… โˆˆ ๐ด) โ†’ (๐‘ฅ โˆˆ ๐ต โ†” (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต)))
7756, 67, 55, 75, 76syl31anc 1372 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ (๐‘ฅ โˆˆ ๐ต โ†” (๐ด ยทo ๐‘ฅ) โˆˆ (๐ด ยทo ๐ต)))
7866, 77mpbird 257 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โˆง ๐‘ฅ โˆˆ On) โ†’ ๐‘ฅ โˆˆ ๐ต)
7978ex 412 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐‘ฅ โˆˆ On โ†’ ๐‘ฅ โˆˆ ๐ต))
8054, 79impbid 211 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘ฆ โˆˆ ๐ด)) โ†’ (๐‘ฅ โˆˆ ๐ต โ†” ๐‘ฅ โˆˆ On))
8180expr 456 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐‘ฆ โˆˆ ๐ด โ†’ (๐‘ฅ โˆˆ ๐ต โ†” ๐‘ฅ โˆˆ On)))
8281pm5.32rd 577 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โˆˆ (๐ด ยทo ๐ต)) โ†’ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โ†” (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด)))
8352, 82sylan2 592 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง (๐‘š โˆˆ (๐ด ยทo ๐ต) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))) โ†’ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โ†” (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด)))
8483expr 456 . . . . . . . . . . . . . 14 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โ†’ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โ†” (๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด))))
8584pm5.32rd 577 . . . . . . . . . . . . 13 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))))
86 eqcom 2738 . . . . . . . . . . . . . 14 (๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) โ†” ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)
8786anbi2i 622 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))
8885, 87bitrdi 287 . . . . . . . . . . . 12 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
8988anbi2d 628 . . . . . . . . . . 11 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ((๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))) โ†” (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))))
90 an12 642 . . . . . . . . . . 11 ((๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
9189, 90bitrdi 287 . . . . . . . . . 10 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ ((๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))) โ†” ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))))
92912exbidv 1926 . . . . . . . . 9 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))) โ†” โˆƒ๐‘ฅโˆƒ๐‘ฆ((๐‘ฅ โˆˆ On โˆง ๐‘ฆ โˆˆ ๐ด) โˆง (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š))))
93 df-mpo 7417 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ ๐ต, ๐‘ฆ โˆˆ ๐ด โ†ฆ ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)) = {โŸจโŸจ๐‘ฅ, ๐‘ฆโŸฉ, ๐‘šโŸฉ โˆฃ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))}
94 dfoprab2 7470 . . . . . . . . . . . 12 {โŸจโŸจ๐‘ฅ, ๐‘ฆโŸฉ, ๐‘šโŸฉ โˆฃ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))} = {โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))}
9528, 93, 943eqtri 2763 . . . . . . . . . . 11 ๐น = {โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))}
9695breqi 5154 . . . . . . . . . 10 (๐‘›๐น๐‘š โ†” ๐‘›{โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))}๐‘š)
97 df-br 5149 . . . . . . . . . 10 (๐‘›{โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))}๐‘š โ†” โŸจ๐‘›, ๐‘šโŸฉ โˆˆ {โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))})
98 opabidw 5524 . . . . . . . . . 10 (โŸจ๐‘›, ๐‘šโŸฉ โˆˆ {โŸจ๐‘›, ๐‘šโŸฉ โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ)))} โ†” โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))))
9996, 97, 983bitri 297 . . . . . . . . 9 (๐‘›๐น๐‘š โ†” โˆƒ๐‘ฅโˆƒ๐‘ฆ(๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ด) โˆง ๐‘š = ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ))))
100 r2ex 3194 . . . . . . . . 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 2579 . . . . . 6 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ (โˆƒ!๐‘› ๐‘šโ—ก๐น๐‘› โ†” โˆƒ!๐‘›โˆƒ๐‘ฅ โˆˆ On โˆƒ๐‘ฆ โˆˆ ๐ด (๐‘› = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง ((๐ด ยทo ๐‘ฅ) +o ๐‘ฆ) = ๐‘š)))
10447, 103mpbird 257 . . . . 5 (((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โˆง ๐‘š โˆˆ (๐ด ยทo ๐ต)) โ†’ โˆƒ!๐‘› ๐‘šโ—ก๐น๐‘›)
105104ralrimiva 3145 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ โˆ€๐‘š โˆˆ (๐ด ยทo ๐ต)โˆƒ!๐‘› ๐‘šโ—ก๐น๐‘›)
106 fnres 6677 . . . 4 ((โ—ก๐น โ†พ (๐ด ยทo ๐ต)) Fn (๐ด ยทo ๐ต) โ†” โˆ€๐‘š โˆˆ (๐ด ยทo ๐ต)โˆƒ!๐‘› ๐‘šโ—ก๐น๐‘›)
107105, 106sylibr 233 . . 3 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (โ—ก๐น โ†พ (๐ด ยทo ๐ต)) Fn (๐ด ยทo ๐ต))
108 relcnv 6103 . . . . 5 Rel โ—ก๐น
109 df-rn 5687 . . . . . 6 ran ๐น = dom โ—ก๐น
11030frnd 6725 . . . . . 6 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ran ๐น โŠ† (๐ด ยทo ๐ต))
111109, 110eqsstrrid 4031 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ dom โ—ก๐น โŠ† (๐ด ยทo ๐ต))
112 relssres 6022 . . . . 5 ((Rel โ—ก๐น โˆง dom โ—ก๐น โŠ† (๐ด ยทo ๐ต)) โ†’ (โ—ก๐น โ†พ (๐ด ยทo ๐ต)) = โ—ก๐น)
113108, 111, 112sylancr 586 . . . 4 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (โ—ก๐น โ†พ (๐ด ยทo ๐ต)) = โ—ก๐น)
114113fneq1d 6642 . . 3 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ((โ—ก๐น โ†พ (๐ด ยทo ๐ต)) Fn (๐ด ยทo ๐ต) โ†” โ—ก๐น Fn (๐ด ยทo ๐ต)))
115107, 114mpbid 231 . 2 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ โ—ก๐น Fn (๐ด ยทo ๐ต))
116 dff1o4 6841 . 2 (๐น:(๐ต ร— ๐ด)โ€“1-1-ontoโ†’(๐ด ยทo ๐ต) โ†” (๐น Fn (๐ต ร— ๐ด) โˆง โ—ก๐น Fn (๐ด ยทo ๐ต)))
11731, 115, 116sylanbrc 582 1 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ ๐น:(๐ต ร— ๐ด)โ€“1-1-ontoโ†’(๐ด ยทo ๐ต))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   = wceq 1540  โˆƒwex 1780   โˆˆ wcel 2105  โˆƒ!weu 2561   โ‰  wne 2939  โˆ€wral 3060  โˆƒwrex 3069   โŠ† wss 3948  โˆ…c0 4322  โŸจcop 4634   class class class wbr 5148  {copab 5210   ร— cxp 5674  โ—กccnv 5675  dom cdm 5676  ran crn 5677   โ†พ cres 5678  Rel wrel 5681  Ord word 6363  Oncon0 6364  suc csuc 6366   Fn wfn 6538  โŸถwf 6539  โ€“1-1-ontoโ†’wf1o 6542  (class class class)co 7412  {coprab 7413   โˆˆ cmpo 7414   +o coa 8467   ยทo comu 8468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-oadd 8474  df-omul 8475
This theorem is referenced by:  omxpen  9078  omf1o  9079  infxpenc  10017
  Copyright terms: Public domain W3C validator