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

Theorem ttukeylem3 10549
Description: Lemma for ttukey 10556. (Contributed by Mario Carneiro, 11-May-2015.)
Hypotheses
Ref Expression
ttukeylem.1 (𝜑𝐹:(card‘( 𝐴𝐵))–1-1-onto→( 𝐴𝐵))
ttukeylem.2 (𝜑𝐵𝐴)
ttukeylem.3 (𝜑 → ∀𝑥(𝑥𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴))
ttukeylem.4 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ran 𝑧), ((𝑧 dom 𝑧) ∪ if(((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴, {(𝐹 dom 𝑧)}, ∅)))))
Assertion
Ref Expression
ttukeylem3 ((𝜑𝐶 ∈ On) → (𝐺𝐶) = if(𝐶 = 𝐶, if(𝐶 = ∅, 𝐵, (𝐺𝐶)), ((𝐺 𝐶) ∪ if(((𝐺 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅))))
Distinct variable groups:   𝑥,𝑧,𝐶   𝑥,𝐺,𝑧   𝜑,𝑧   𝑥,𝐴,𝑧   𝑥,𝐵,𝑧   𝑥,𝐹,𝑧
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ttukeylem3
StepHypRef Expression
1 ttukeylem.4 . . . 4 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ran 𝑧), ((𝑧 dom 𝑧) ∪ if(((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴, {(𝐹 dom 𝑧)}, ∅)))))
21tfr2 8437 . . 3 (𝐶 ∈ On → (𝐺𝐶) = ((𝑧 ∈ V ↦ if(dom 𝑧 = dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ran 𝑧), ((𝑧 dom 𝑧) ∪ if(((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴, {(𝐹 dom 𝑧)}, ∅))))‘(𝐺𝐶)))
32adantl 481 . 2 ((𝜑𝐶 ∈ On) → (𝐺𝐶) = ((𝑧 ∈ V ↦ if(dom 𝑧 = dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ran 𝑧), ((𝑧 dom 𝑧) ∪ if(((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴, {(𝐹 dom 𝑧)}, ∅))))‘(𝐺𝐶)))
4 eqidd 2736 . . 3 ((𝜑𝐶 ∈ On) → (𝑧 ∈ V ↦ if(dom 𝑧 = dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ran 𝑧), ((𝑧 dom 𝑧) ∪ if(((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴, {(𝐹 dom 𝑧)}, ∅)))) = (𝑧 ∈ V ↦ if(dom 𝑧 = dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ran 𝑧), ((𝑧 dom 𝑧) ∪ if(((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴, {(𝐹 dom 𝑧)}, ∅)))))
5 simpr 484 . . . . . . . 8 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → 𝑧 = (𝐺𝐶))
65dmeqd 5919 . . . . . . 7 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → dom 𝑧 = dom (𝐺𝐶))
71tfr1 8436 . . . . . . . . 9 𝐺 Fn On
8 onss 7804 . . . . . . . . . 10 (𝐶 ∈ On → 𝐶 ⊆ On)
98ad2antlr 727 . . . . . . . . 9 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → 𝐶 ⊆ On)
10 fnssres 6692 . . . . . . . . 9 ((𝐺 Fn On ∧ 𝐶 ⊆ On) → (𝐺𝐶) Fn 𝐶)
117, 9, 10sylancr 587 . . . . . . . 8 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → (𝐺𝐶) Fn 𝐶)
1211fndmd 6674 . . . . . . 7 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → dom (𝐺𝐶) = 𝐶)
136, 12eqtrd 2775 . . . . . 6 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → dom 𝑧 = 𝐶)
1413unieqd 4925 . . . . . 6 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → dom 𝑧 = 𝐶)
1513, 14eqeq12d 2751 . . . . 5 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → (dom 𝑧 = dom 𝑧𝐶 = 𝐶))
1613eqeq1d 2737 . . . . . 6 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → (dom 𝑧 = ∅ ↔ 𝐶 = ∅))
175rneqd 5952 . . . . . . . 8 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → ran 𝑧 = ran (𝐺𝐶))
18 df-ima 5702 . . . . . . . 8 (𝐺𝐶) = ran (𝐺𝐶)
1917, 18eqtr4di 2793 . . . . . . 7 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → ran 𝑧 = (𝐺𝐶))
2019unieqd 4925 . . . . . 6 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → ran 𝑧 = (𝐺𝐶))
2116, 20ifbieq2d 4557 . . . . 5 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → if(dom 𝑧 = ∅, 𝐵, ran 𝑧) = if(𝐶 = ∅, 𝐵, (𝐺𝐶)))
225, 14fveq12d 6914 . . . . . 6 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → (𝑧 dom 𝑧) = ((𝐺𝐶)‘ 𝐶))
2314fveq2d 6911 . . . . . . . . . 10 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → (𝐹 dom 𝑧) = (𝐹 𝐶))
2423sneqd 4643 . . . . . . . . 9 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → {(𝐹 dom 𝑧)} = {(𝐹 𝐶)})
2522, 24uneq12d 4179 . . . . . . . 8 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → ((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) = (((𝐺𝐶)‘ 𝐶) ∪ {(𝐹 𝐶)}))
2625eleq1d 2824 . . . . . . 7 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → (((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴 ↔ (((𝐺𝐶)‘ 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴))
27 eqidd 2736 . . . . . . 7 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → ∅ = ∅)
2826, 24, 27ifbieq12d 4559 . . . . . 6 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → if(((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴, {(𝐹 dom 𝑧)}, ∅) = if((((𝐺𝐶)‘ 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅))
2922, 28uneq12d 4179 . . . . 5 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → ((𝑧 dom 𝑧) ∪ if(((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴, {(𝐹 dom 𝑧)}, ∅)) = (((𝐺𝐶)‘ 𝐶) ∪ if((((𝐺𝐶)‘ 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅)))
3015, 21, 29ifbieq12d 4559 . . . 4 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → if(dom 𝑧 = dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ran 𝑧), ((𝑧 dom 𝑧) ∪ if(((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴, {(𝐹 dom 𝑧)}, ∅))) = if(𝐶 = 𝐶, if(𝐶 = ∅, 𝐵, (𝐺𝐶)), (((𝐺𝐶)‘ 𝐶) ∪ if((((𝐺𝐶)‘ 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅))))
31 onuni 7808 . . . . . . . . . 10 (𝐶 ∈ On → 𝐶 ∈ On)
3231ad3antlr 731 . . . . . . . . 9 ((((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 ∈ On)
33 sucidg 6467 . . . . . . . . 9 ( 𝐶 ∈ On → 𝐶 ∈ suc 𝐶)
3432, 33syl 17 . . . . . . . 8 ((((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 ∈ suc 𝐶)
35 eloni 6396 . . . . . . . . . . 11 (𝐶 ∈ On → Ord 𝐶)
3635ad2antlr 727 . . . . . . . . . 10 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → Ord 𝐶)
37 orduniorsuc 7850 . . . . . . . . . 10 (Ord 𝐶 → (𝐶 = 𝐶𝐶 = suc 𝐶))
3836, 37syl 17 . . . . . . . . 9 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → (𝐶 = 𝐶𝐶 = suc 𝐶))
3938orcanai 1004 . . . . . . . 8 ((((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶 = suc 𝐶)
4034, 39eleqtrrd 2842 . . . . . . 7 ((((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) ∧ ¬ 𝐶 = 𝐶) → 𝐶𝐶)
4140fvresd 6927 . . . . . 6 ((((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) ∧ ¬ 𝐶 = 𝐶) → ((𝐺𝐶)‘ 𝐶) = (𝐺 𝐶))
4241uneq1d 4177 . . . . . . . 8 ((((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) ∧ ¬ 𝐶 = 𝐶) → (((𝐺𝐶)‘ 𝐶) ∪ {(𝐹 𝐶)}) = ((𝐺 𝐶) ∪ {(𝐹 𝐶)}))
4342eleq1d 2824 . . . . . . 7 ((((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) ∧ ¬ 𝐶 = 𝐶) → ((((𝐺𝐶)‘ 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴 ↔ ((𝐺 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴))
4443ifbid 4554 . . . . . 6 ((((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) ∧ ¬ 𝐶 = 𝐶) → if((((𝐺𝐶)‘ 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅) = if(((𝐺 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅))
4541, 44uneq12d 4179 . . . . 5 ((((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) ∧ ¬ 𝐶 = 𝐶) → (((𝐺𝐶)‘ 𝐶) ∪ if((((𝐺𝐶)‘ 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅)) = ((𝐺 𝐶) ∪ if(((𝐺 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅)))
4645ifeq2da 4563 . . . 4 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → if(𝐶 = 𝐶, if(𝐶 = ∅, 𝐵, (𝐺𝐶)), (((𝐺𝐶)‘ 𝐶) ∪ if((((𝐺𝐶)‘ 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅))) = if(𝐶 = 𝐶, if(𝐶 = ∅, 𝐵, (𝐺𝐶)), ((𝐺 𝐶) ∪ if(((𝐺 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅))))
4730, 46eqtrd 2775 . . 3 (((𝜑𝐶 ∈ On) ∧ 𝑧 = (𝐺𝐶)) → if(dom 𝑧 = dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ran 𝑧), ((𝑧 dom 𝑧) ∪ if(((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴, {(𝐹 dom 𝑧)}, ∅))) = if(𝐶 = 𝐶, if(𝐶 = ∅, 𝐵, (𝐺𝐶)), ((𝐺 𝐶) ∪ if(((𝐺 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅))))
48 fnfun 6669 . . . . 5 (𝐺 Fn On → Fun 𝐺)
497, 48ax-mp 5 . . . 4 Fun 𝐺
50 simpr 484 . . . 4 ((𝜑𝐶 ∈ On) → 𝐶 ∈ On)
51 resfunexg 7235 . . . 4 ((Fun 𝐺𝐶 ∈ On) → (𝐺𝐶) ∈ V)
5249, 50, 51sylancr 587 . . 3 ((𝜑𝐶 ∈ On) → (𝐺𝐶) ∈ V)
53 ttukeylem.2 . . . . . 6 (𝜑𝐵𝐴)
5453elexd 3502 . . . . 5 (𝜑𝐵 ∈ V)
55 funimaexg 6654 . . . . . . 7 ((Fun 𝐺𝐶 ∈ On) → (𝐺𝐶) ∈ V)
5649, 55mpan 690 . . . . . 6 (𝐶 ∈ On → (𝐺𝐶) ∈ V)
5756uniexd 7761 . . . . 5 (𝐶 ∈ On → (𝐺𝐶) ∈ V)
58 ifcl 4576 . . . . 5 ((𝐵 ∈ V ∧ (𝐺𝐶) ∈ V) → if(𝐶 = ∅, 𝐵, (𝐺𝐶)) ∈ V)
5954, 57, 58syl2an 596 . . . 4 ((𝜑𝐶 ∈ On) → if(𝐶 = ∅, 𝐵, (𝐺𝐶)) ∈ V)
60 fvex 6920 . . . . 5 (𝐺 𝐶) ∈ V
61 snex 5442 . . . . . 6 {(𝐹 𝐶)} ∈ V
62 0ex 5313 . . . . . 6 ∅ ∈ V
6361, 62ifex 4581 . . . . 5 if(((𝐺 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅) ∈ V
6460, 63unex 7763 . . . 4 ((𝐺 𝐶) ∪ if(((𝐺 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅)) ∈ V
65 ifcl 4576 . . . 4 ((if(𝐶 = ∅, 𝐵, (𝐺𝐶)) ∈ V ∧ ((𝐺 𝐶) ∪ if(((𝐺 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅)) ∈ V) → if(𝐶 = 𝐶, if(𝐶 = ∅, 𝐵, (𝐺𝐶)), ((𝐺 𝐶) ∪ if(((𝐺 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅))) ∈ V)
6659, 64, 65sylancl 586 . . 3 ((𝜑𝐶 ∈ On) → if(𝐶 = 𝐶, if(𝐶 = ∅, 𝐵, (𝐺𝐶)), ((𝐺 𝐶) ∪ if(((𝐺 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅))) ∈ V)
674, 47, 52, 66fvmptd 7023 . 2 ((𝜑𝐶 ∈ On) → ((𝑧 ∈ V ↦ if(dom 𝑧 = dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ran 𝑧), ((𝑧 dom 𝑧) ∪ if(((𝑧 dom 𝑧) ∪ {(𝐹 dom 𝑧)}) ∈ 𝐴, {(𝐹 dom 𝑧)}, ∅))))‘(𝐺𝐶)) = if(𝐶 = 𝐶, if(𝐶 = ∅, 𝐵, (𝐺𝐶)), ((𝐺 𝐶) ∪ if(((𝐺 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅))))
683, 67eqtrd 2775 1 ((𝜑𝐶 ∈ On) → (𝐺𝐶) = if(𝐶 = 𝐶, if(𝐶 = ∅, 𝐵, (𝐺𝐶)), ((𝐺 𝐶) ∪ if(((𝐺 𝐶) ∪ {(𝐹 𝐶)}) ∈ 𝐴, {(𝐹 𝐶)}, ∅))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  wal 1535   = wceq 1537  wcel 2106  Vcvv 3478  cdif 3960  cun 3961  cin 3962  wss 3963  c0 4339  ifcif 4531  𝒫 cpw 4605  {csn 4631   cuni 4912  cmpt 5231  dom cdm 5689  ran crn 5690  cres 5691  cima 5692  Ord word 6385  Oncon0 6386  suc csuc 6388  Fun wfun 6557   Fn wfn 6558  1-1-ontowf1o 6562  cfv 6563  recscrecs 8409  Fincfn 8984  cardccrd 9973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410
This theorem is referenced by:  ttukeylem4  10550  ttukeylem5  10551  ttukeylem6  10552  ttukeylem7  10553
  Copyright terms: Public domain W3C validator