New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  sbthlem1 GIF version

Theorem sbthlem1 6203
 Description: Lemma for sbth 6206. Set up similarity with a range. Theorem XI.1.14 of [Rosser] p. 350. (Contributed by SF, 11-Mar-2015.)
Hypotheses
Ref Expression
sbthlem1.1 R V
sbthlem1.2 X V
sbthlem1.3 G = Clos1 ((X ran R), R)
sbthlem1.4 A = (XG)
sbthlem1.5 B = (X G)
sbthlem1.6 C = (ran RG)
sbthlem1.7 D = (ran R G)
Assertion
Ref Expression
sbthlem1 (((Fun R Fun R) (X dom R ran R X)) → ran RX)

Proof of Theorem sbthlem1
StepHypRef Expression
1 df-f1 4792 . . . . . . . . 9 (R:dom R1-1→ran R ↔ (R:dom R–→ran R Fun R))
2 ssid 3290 . . . . . . . . . . . 12 ran R ran R
3 df-f 4791 . . . . . . . . . . . 12 (R:dom R–→ran R ↔ (R Fn dom R ran R ran R))
42, 3mpbiran2 885 . . . . . . . . . . 11 (R:dom R–→ran RR Fn dom R)
5 funfn 5136 . . . . . . . . . . 11 (Fun RR Fn dom R)
64, 5bitr4i 243 . . . . . . . . . 10 (R:dom R–→ran R ↔ Fun R)
76anbi1i 676 . . . . . . . . 9 ((R:dom R–→ran R Fun R) ↔ (Fun R Fun R))
81, 7bitri 240 . . . . . . . 8 (R:dom R1-1→ran R ↔ (Fun R Fun R))
98biimpri 197 . . . . . . 7 ((Fun R Fun R) → R:dom R1-1→ran R)
10 sbthlem1.4 . . . . . . . . 9 A = (XG)
11 inss1 3475 . . . . . . . . . 10 (XG) X
12 sstr 3280 . . . . . . . . . 10 (((XG) X X dom R) → (XG) dom R)
1311, 12mpan 651 . . . . . . . . 9 (X dom R → (XG) dom R)
1410, 13syl5eqss 3315 . . . . . . . 8 (X dom RA dom R)
1514adantr 451 . . . . . . 7 ((X dom R ran R X) → A dom R)
16 f1ores 5300 . . . . . . 7 ((R:dom R1-1→ran R A dom R) → (R A):A1-1-onto→(RA))
179, 15, 16syl2an 463 . . . . . 6 (((Fun R Fun R) (X dom R ran R X)) → (R A):A1-1-onto→(RA))
18 sbthlem1.1 . . . . . . . 8 R V
19 sbthlem1.2 . . . . . . . . . 10 X V
20 sbthlem1.3 . . . . . . . . . . 11 G = Clos1 ((X ran R), R)
2118rnex 5107 . . . . . . . . . . . . 13 ran R V
2219, 21difex 4107 . . . . . . . . . . . 12 (X ran R) V
2322, 18clos1ex 5876 . . . . . . . . . . 11 Clos1 ((X ran R), R) V
2420, 23eqeltri 2423 . . . . . . . . . 10 G V
2519, 24inex 4105 . . . . . . . . 9 (XG) V
2610, 25eqeltri 2423 . . . . . . . 8 A V
2718, 26resex 5117 . . . . . . 7 (R A) V
2827f1oen 6033 . . . . . 6 ((R A):A1-1-onto→(RA) → A ≈ (RA))
2917, 28syl 15 . . . . 5 (((Fun R Fun R) (X dom R ran R X)) → A ≈ (RA))
30 sbthlem1.6 . . . . . . . . 9 C = (ran RG)
3122, 18, 20clos1baseima 5883 . . . . . . . . . 10 G = ((X ran R) ∪ (RG))
3231ineq2i 3454 . . . . . . . . 9 (ran RG) = (ran R ∩ ((X ran R) ∪ (RG)))
33 indi 3501 . . . . . . . . . 10 (ran R ∩ ((X ran R) ∪ (RG))) = ((ran R ∩ (X ran R)) ∪ (ran R ∩ (RG)))
34 disjdif 3622 . . . . . . . . . . 11 (ran R ∩ (X ran R)) =
3534uneq1i 3414 . . . . . . . . . 10 ((ran R ∩ (X ran R)) ∪ (ran R ∩ (RG))) = ( ∪ (ran R ∩ (RG)))
36 uncom 3408 . . . . . . . . . . 11 ( ∪ (ran R ∩ (RG))) = ((ran R ∩ (RG)) ∪ )
37 un0 3575 . . . . . . . . . . 11 ((ran R ∩ (RG)) ∪ ) = (ran R ∩ (RG))
3836, 37eqtri 2373 . . . . . . . . . 10 ( ∪ (ran R ∩ (RG))) = (ran R ∩ (RG))
3933, 35, 383eqtri 2377 . . . . . . . . 9 (ran R ∩ ((X ran R) ∪ (RG))) = (ran R ∩ (RG))
4030, 32, 393eqtri 2377 . . . . . . . 8 C = (ran R ∩ (RG))
41 inss2 3476 . . . . . . . . 9 (ran R ∩ (RG)) (RG)
4241a1i 10 . . . . . . . 8 (((Fun R Fun R) (X dom R ran R X)) → (ran R ∩ (RG)) (RG))
4340, 42syl5eqss 3315 . . . . . . 7 (((Fun R Fun R) (X dom R ran R X)) → C (RG))
44 imassrn 5009 . . . . . . . . . . . . . 14 (RG) ran R
45 simprr 733 . . . . . . . . . . . . . 14 (((Fun R Fun R) (X dom R ran R X)) → ran R X)
4644, 45syl5ss 3283 . . . . . . . . . . . . 13 (((Fun R Fun R) (X dom R ran R X)) → (RG) X)
47 difss 3393 . . . . . . . . . . . . 13 (X ran R) X
4846, 47jctil 523 . . . . . . . . . . . 12 (((Fun R Fun R) (X dom R ran R X)) → ((X ran R) X (RG) X))
49 unss 3437 . . . . . . . . . . . 12 (((X ran R) X (RG) X) ↔ ((X ran R) ∪ (RG)) X)
5048, 49sylib 188 . . . . . . . . . . 11 (((Fun R Fun R) (X dom R ran R X)) → ((X ran R) ∪ (RG)) X)
5131, 50syl5eqss 3315 . . . . . . . . . 10 (((Fun R Fun R) (X dom R ran R X)) → G X)
52 sseqin2 3474 . . . . . . . . . 10 (G X ↔ (XG) = G)
5351, 52sylib 188 . . . . . . . . 9 (((Fun R Fun R) (X dom R ran R X)) → (XG) = G)
5410, 53syl5eq 2397 . . . . . . . 8 (((Fun R Fun R) (X dom R ran R X)) → A = G)
5554imaeq2d 4942 . . . . . . 7 (((Fun R Fun R) (X dom R ran R X)) → (RA) = (RG))
5643, 55sseqtr4d 3308 . . . . . 6 (((Fun R Fun R) (X dom R ran R X)) → C (RA))
57 ssun2 3427 . . . . . . . . . . 11 (RG) ((X ran R) ∪ (RG))
5857, 31sseqtr4i 3304 . . . . . . . . . 10 (RG) G
5955sseq1d 3298 . . . . . . . . . 10 (((Fun R Fun R) (X dom R ran R X)) → ((RA) G ↔ (RG) G))
6058, 59mpbiri 224 . . . . . . . . 9 (((Fun R Fun R) (X dom R ran R X)) → (RA) G)
61 imassrn 5009 . . . . . . . . 9 (RA) ran R
6260, 61jctil 523 . . . . . . . 8 (((Fun R Fun R) (X dom R ran R X)) → ((RA) ran R (RA) G))
63 ssin 3477 . . . . . . . 8 (((RA) ran R (RA) G) ↔ (RA) (ran RG))
6462, 63sylib 188 . . . . . . 7 (((Fun R Fun R) (X dom R ran R X)) → (RA) (ran RG))
6564, 30syl6sseqr 3318 . . . . . 6 (((Fun R Fun R) (X dom R ran R X)) → (RA) C)
6656, 65eqssd 3289 . . . . 5 (((Fun R Fun R) (X dom R ran R X)) → C = (RA))
6729, 66breqtrrd 4665 . . . 4 (((Fun R Fun R) (X dom R ran R X)) → AC)
68 sbthlem1.5 . . . . . . 7 B = (X G)
6919, 24difex 4107 . . . . . . 7 (X G) V
7068, 69eqeltri 2423 . . . . . 6 B V
7170enrflx 6035 . . . . 5 BB
72 difsscompl 3549 . . . . . . . . . 10 (X G) G
7372a1i 10 . . . . . . . . 9 (((Fun R Fun R) (X dom R ran R X)) → (X G) G)
74 df-dif 3215 . . . . . . . . . . 11 (X G) = (X ∩ ∼ G)
7520clos1base 5878 . . . . . . . . . . . . . 14 (X ran R) G
76 sscon34 3661 . . . . . . . . . . . . . 14 ((X ran R) G ↔ ∼ G ∼ (X ran R))
7775, 76mpbi 199 . . . . . . . . . . . . 13 G ∼ (X ran R)
78 df-dif 3215 . . . . . . . . . . . . . . 15 (X ran R) = (X ∩ ∼ ran R)
7978compleqi 3244 . . . . . . . . . . . . . 14 ∼ (X ran R) = ∼ (X ∩ ∼ ran R)
80 iinun 3548 . . . . . . . . . . . . . 14 ∼ (X ∩ ∼ ran R) = ( ∼ X ∪ ∼ ∼ ran R)
81 dblcompl 3227 . . . . . . . . . . . . . . 15 ∼ ∼ ran R = ran R
8281uneq2i 3415 . . . . . . . . . . . . . 14 ( ∼ X ∪ ∼ ∼ ran R) = ( ∼ X ∪ ran R)
8379, 80, 823eqtri 2377 . . . . . . . . . . . . 13 ∼ (X ran R) = ( ∼ X ∪ ran R)
8477, 83sseqtri 3303 . . . . . . . . . . . 12 G ( ∼ X ∪ ran R)
85 sslin 3481 . . . . . . . . . . . 12 ( ∼ G ( ∼ X ∪ ran R) → (X ∩ ∼ G) (X ∩ ( ∼ X ∪ ran R)))
8684, 85ax-mp 5 . . . . . . . . . . 11 (X ∩ ∼ G) (X ∩ ( ∼ X ∪ ran R))
8774, 86eqsstri 3301 . . . . . . . . . 10 (X G) (X ∩ ( ∼ X ∪ ran R))
88 indi 3501 . . . . . . . . . . . 12 (X ∩ ( ∼ X ∪ ran R)) = ((X ∩ ∼ X) ∪ (X ∩ ran R))
89 incompl 4073 . . . . . . . . . . . . 13 (X ∩ ∼ X) =
9089uneq1i 3414 . . . . . . . . . . . 12 ((X ∩ ∼ X) ∪ (X ∩ ran R)) = ( ∪ (X ∩ ran R))
91 uncom 3408 . . . . . . . . . . . . 13 ( ∪ (X ∩ ran R)) = ((X ∩ ran R) ∪ )
92 un0 3575 . . . . . . . . . . . . 13 ((X ∩ ran R) ∪ ) = (X ∩ ran R)
9391, 92eqtri 2373 . . . . . . . . . . . 12 ( ∪ (X ∩ ran R)) = (X ∩ ran R)
9488, 90, 933eqtri 2377 . . . . . . . . . . 11 (X ∩ ( ∼ X ∪ ran R)) = (X ∩ ran R)
95 inss2 3476 . . . . . . . . . . 11 (X ∩ ran R) ran R
9694, 95eqsstri 3301 . . . . . . . . . 10 (X ∩ ( ∼ X ∪ ran R)) ran R
9787, 96sstri 3281 . . . . . . . . 9 (X G) ran R
9873, 97jctil 523 . . . . . . . 8 (((Fun R Fun R) (X dom R ran R X)) → ((X G) ran R (X G) G))
99 ssin 3477 . . . . . . . 8 (((X G) ran R (X G) G) ↔ (X G) (ran R ∩ ∼ G))
10098, 99sylib 188 . . . . . . 7 (((Fun R Fun R) (X dom R ran R X)) → (X G) (ran R ∩ ∼ G))
101 sbthlem1.7 . . . . . . . 8 D = (ran R G)
102 df-dif 3215 . . . . . . . 8 (ran R G) = (ran R ∩ ∼ G)
103101, 102eqtri 2373 . . . . . . 7 D = (ran R ∩ ∼ G)
104100, 68, 1033sstr4g 3312 . . . . . 6 (((Fun R Fun R) (X dom R ran R X)) → B D)
105 ssdif 3401 . . . . . . . 8 (ran R X → (ran R G) (X G))
10645, 105syl 15 . . . . . . 7 (((Fun R Fun R) (X dom R ran R X)) → (ran R G) (X G))
107106, 101, 683sstr4g 3312 . . . . . 6 (((Fun R Fun R) (X dom R ran R X)) → D B)
108104, 107eqssd 3289 . . . . 5 (((Fun R Fun R) (X dom R ran R X)) → B = D)
10971, 108syl5breq 4674 . . . 4 (((Fun R Fun R) (X dom R ran R X)) → BD)
11010, 68ineq12i 3455 . . . . . 6 (AB) = ((XG) ∩ (X G))
111 inindif 4075 . . . . . 6 ((XG) ∩ (X G)) =
112110, 111eqtri 2373 . . . . 5 (AB) =
11330, 101ineq12i 3455 . . . . . 6 (CD) = ((ran RG) ∩ (ran R G))
114 inindif 4075 . . . . . 6 ((ran RG) ∩ (ran R G)) =
115113, 114eqtri 2373 . . . . 5 (CD) =
116 unen 6048 . . . . 5 (((AC BD) ((AB) = (CD) = )) → (AB) ≈ (CD))
117112, 115, 116mpanr12 666 . . . 4 ((AC BD) → (AB) ≈ (CD))
11867, 109, 117syl2anc 642 . . 3 (((Fun R Fun R) (X dom R ran R X)) → (AB) ≈ (CD))
119 ensym 6037 . . 3 ((AB) ≈ (CD) ↔ (CD) ≈ (AB))
120118, 119sylib 188 . 2 (((Fun R Fun R) (X dom R ran R X)) → (CD) ≈ (AB))
12130, 101uneq12i 3416 . . 3 (CD) = ((ran RG) ∪ (ran R G))
122 inundif 3628 . . 3 ((ran RG) ∪ (ran R G)) = ran R
123121, 122eqtri 2373 . 2 (CD) = ran R
12410, 68uneq12i 3416 . . 3 (AB) = ((XG) ∪ (X G))
125 inundif 3628 . . 3 ((XG) ∪ (X G)) = X
126124, 125eqtri 2373 . 2 (AB) = X
127120, 123, 1263brtr3g 4670 1 (((Fun R Fun R) (X dom R ran R X)) → ran RX)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   = wceq 1642   ∈ wcel 1710  Vcvv 2859   ∼ ccompl 3205   ∖ cdif 3206   ∪ cun 3207   ∩ cin 3208   ⊆ wss 3257  ∅c0 3550   class class class wbr 4639   “ cima 4722  ◡ccnv 4771  dom cdm 4772  ran crn 4773   ↾ cres 4774  Fun wfun 4775   Fn wfn 4776  –→wf 4777  –1-1→wf1 4778  –1-1-onto→wf1o 4780   Clos1 cclos1 5872   ≈ cen 6028 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-id 4767  df-xp 4784  df-cnv 4785  df-rn 4786  df-dm 4787  df-res 4788  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794  df-2nd 4797  df-txp 5736  df-fix 5740  df-ins2 5750  df-ins3 5752  df-image 5754  df-clos1 5873  df-en 6029 This theorem is referenced by:  sbthlem2  6204
 Copyright terms: Public domain W3C validator