ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ac6sfi GIF version

Theorem ac6sfi 6912
Description: Existence of a choice function for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
Hypothesis
Ref Expression
ac6sfi.1 (𝑦 = (π‘“β€˜π‘₯) β†’ (πœ‘ ↔ πœ“))
Assertion
Ref Expression
ac6sfi ((𝐴 ∈ Fin ∧ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐡 πœ‘) β†’ βˆƒπ‘“(𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“))
Distinct variable groups:   π‘₯,𝑓,𝐴   𝑦,𝑓,𝐡,π‘₯   πœ‘,𝑓   πœ“,𝑦
Allowed substitution hints:   πœ‘(π‘₯,𝑦)   πœ“(π‘₯,𝑓)   𝐴(𝑦)

Proof of Theorem ac6sfi
Dummy variables 𝑒 𝑀 𝑧 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 raleq 2683 . . . 4 (𝑒 = βˆ… β†’ (βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆ€π‘₯ ∈ βˆ… βˆƒπ‘¦ ∈ 𝐡 πœ‘))
2 feq2 5361 . . . . . 6 (𝑒 = βˆ… β†’ (𝑓:π‘’βŸΆπ΅ ↔ 𝑓:βˆ…βŸΆπ΅))
3 raleq 2683 . . . . . 6 (𝑒 = βˆ… β†’ (βˆ€π‘₯ ∈ 𝑒 πœ“ ↔ βˆ€π‘₯ ∈ βˆ… πœ“))
42, 3anbi12d 473 . . . . 5 (𝑒 = βˆ… β†’ ((𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ (𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“)))
54exbidv 1835 . . . 4 (𝑒 = βˆ… β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘“(𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“)))
61, 5imbi12d 234 . . 3 (𝑒 = βˆ… β†’ ((βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“)) ↔ (βˆ€π‘₯ ∈ βˆ… βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“))))
7 raleq 2683 . . . 4 (𝑒 = 𝑀 β†’ (βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘))
8 feq2 5361 . . . . . 6 (𝑒 = 𝑀 β†’ (𝑓:π‘’βŸΆπ΅ ↔ 𝑓:π‘€βŸΆπ΅))
9 raleq 2683 . . . . . 6 (𝑒 = 𝑀 β†’ (βˆ€π‘₯ ∈ 𝑒 πœ“ ↔ βˆ€π‘₯ ∈ 𝑀 πœ“))
108, 9anbi12d 473 . . . . 5 (𝑒 = 𝑀 β†’ ((𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)))
1110exbidv 1835 . . . 4 (𝑒 = 𝑀 β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)))
127, 11imbi12d 234 . . 3 (𝑒 = 𝑀 β†’ ((βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“)) ↔ (βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“))))
13 raleq 2683 . . . 4 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘))
14 feq2 5361 . . . . . . 7 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (𝑓:π‘’βŸΆπ΅ ↔ 𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡))
15 raleq 2683 . . . . . . 7 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (βˆ€π‘₯ ∈ 𝑒 πœ“ ↔ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“))
1614, 15anbi12d 473 . . . . . 6 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ ((𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ (𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“)))
1716exbidv 1835 . . . . 5 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘“(𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“)))
18 feq1 5360 . . . . . . 7 (𝑓 = 𝑔 β†’ (𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ↔ 𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡))
19 vex 2752 . . . . . . . . . . 11 𝑓 ∈ V
20 vex 2752 . . . . . . . . . . 11 π‘₯ ∈ V
2119, 20fvex 5547 . . . . . . . . . 10 (π‘“β€˜π‘₯) ∈ V
22 ac6sfi.1 . . . . . . . . . 10 (𝑦 = (π‘“β€˜π‘₯) β†’ (πœ‘ ↔ πœ“))
2321, 22sbcie 3009 . . . . . . . . 9 ([(π‘“β€˜π‘₯) / 𝑦]πœ‘ ↔ πœ“)
24 fveq1 5526 . . . . . . . . . 10 (𝑓 = 𝑔 β†’ (π‘“β€˜π‘₯) = (π‘”β€˜π‘₯))
2524sbceq1d 2979 . . . . . . . . 9 (𝑓 = 𝑔 β†’ ([(π‘“β€˜π‘₯) / 𝑦]πœ‘ ↔ [(π‘”β€˜π‘₯) / 𝑦]πœ‘))
2623, 25bitr3id 194 . . . . . . . 8 (𝑓 = 𝑔 β†’ (πœ“ ↔ [(π‘”β€˜π‘₯) / 𝑦]πœ‘))
2726ralbidv 2487 . . . . . . 7 (𝑓 = 𝑔 β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“ ↔ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
2818, 27anbi12d 473 . . . . . 6 (𝑓 = 𝑔 β†’ ((𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“) ↔ (𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))
2928cbvexv 1928 . . . . 5 (βˆƒπ‘“(𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“) ↔ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
3017, 29bitrdi 196 . . . 4 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))
3113, 30imbi12d 234 . . 3 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ ((βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“)) ↔ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
32 raleq 2683 . . . 4 (𝑒 = 𝐴 β†’ (βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐡 πœ‘))
33 feq2 5361 . . . . . 6 (𝑒 = 𝐴 β†’ (𝑓:π‘’βŸΆπ΅ ↔ 𝑓:𝐴⟢𝐡))
34 raleq 2683 . . . . . 6 (𝑒 = 𝐴 β†’ (βˆ€π‘₯ ∈ 𝑒 πœ“ ↔ βˆ€π‘₯ ∈ 𝐴 πœ“))
3533, 34anbi12d 473 . . . . 5 (𝑒 = 𝐴 β†’ ((𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ (𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“)))
3635exbidv 1835 . . . 4 (𝑒 = 𝐴 β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘“(𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“)))
3732, 36imbi12d 234 . . 3 (𝑒 = 𝐴 β†’ ((βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“)) ↔ (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“))))
38 f0 5418 . . . 4 βˆ…:βˆ…βŸΆπ΅
39 0ex 4142 . . . . 5 βˆ… ∈ V
40 ral0 3536 . . . . . . 7 βˆ€π‘₯ ∈ βˆ… πœ“
4140biantru 302 . . . . . 6 (𝑓:βˆ…βŸΆπ΅ ↔ (𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“))
42 feq1 5360 . . . . . 6 (𝑓 = βˆ… β†’ (𝑓:βˆ…βŸΆπ΅ ↔ βˆ…:βˆ…βŸΆπ΅))
4341, 42bitr3id 194 . . . . 5 (𝑓 = βˆ… β†’ ((𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“) ↔ βˆ…:βˆ…βŸΆπ΅))
4439, 43spcev 2844 . . . 4 (βˆ…:βˆ…βŸΆπ΅ β†’ βˆƒπ‘“(𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“))
4538, 44mp1i 10 . . 3 (βˆ€π‘₯ ∈ βˆ… βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“))
46 ssun1 3310 . . . . . . 7 𝑀 βŠ† (𝑀 βˆͺ {𝑧})
47 ssralv 3231 . . . . . . 7 (𝑀 βŠ† (𝑀 βˆͺ {𝑧}) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘))
4846, 47ax-mp 5 . . . . . 6 (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘)
4948imim1i 60 . . . . 5 ((βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)))
50 ssun2 3311 . . . . . . . . 9 {𝑧} βŠ† (𝑀 βˆͺ {𝑧})
51 ssralv 3231 . . . . . . . . 9 ({𝑧} βŠ† (𝑀 βˆͺ {𝑧}) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘))
5250, 51ax-mp 5 . . . . . . . 8 (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘)
53 vex 2752 . . . . . . . . . 10 𝑧 ∈ V
54 ralsnsg 3641 . . . . . . . . . 10 (𝑧 ∈ V β†’ (βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ [𝑧 / π‘₯]βˆƒπ‘¦ ∈ 𝐡 πœ‘))
5553, 54ax-mp 5 . . . . . . . . 9 (βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ [𝑧 / π‘₯]βˆƒπ‘¦ ∈ 𝐡 πœ‘)
56 sbcrex 3054 . . . . . . . . 9 ([𝑧 / π‘₯]βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆƒπ‘¦ ∈ 𝐡 [𝑧 / π‘₯]πœ‘)
5755, 56bitri 184 . . . . . . . 8 (βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆƒπ‘¦ ∈ 𝐡 [𝑧 / π‘₯]πœ‘)
5852, 57sylib 122 . . . . . . 7 (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘¦ ∈ 𝐡 [𝑧 / π‘₯]πœ‘)
59 nfv 1538 . . . . . . . 8 Ⅎ𝑦 Β¬ 𝑧 ∈ 𝑀
60 nfv 1538 . . . . . . . . 9 β„²π‘¦βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)
61 nfv 1538 . . . . . . . . . . 11 Ⅎ𝑦 𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡
62 nfcv 2329 . . . . . . . . . . . 12 Ⅎ𝑦(𝑀 βˆͺ {𝑧})
63 nfsbc1v 2993 . . . . . . . . . . . 12 Ⅎ𝑦[(π‘”β€˜π‘₯) / 𝑦]πœ‘
6462, 63nfralxy 2525 . . . . . . . . . . 11 β„²π‘¦βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘
6561, 64nfan 1575 . . . . . . . . . 10 Ⅎ𝑦(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)
6665nfex 1647 . . . . . . . . 9 β„²π‘¦βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)
6760, 66nfim 1582 . . . . . . . 8 Ⅎ𝑦(βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
68 simprl 529 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ 𝑓:π‘€βŸΆπ΅)
69 vex 2752 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
7053, 69f1osn 5513 . . . . . . . . . . . . . . 15 {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}–1-1-ontoβ†’{𝑦}
71 f1of 5473 . . . . . . . . . . . . . . 15 ({βŸ¨π‘§, π‘¦βŸ©}:{𝑧}–1-1-ontoβ†’{𝑦} β†’ {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}⟢{𝑦})
7270, 71mp1i 10 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}⟢{𝑦})
73 simpl2 1002 . . . . . . . . . . . . . . 15 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ 𝑦 ∈ 𝐡)
7473snssd 3749 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ {𝑦} βŠ† 𝐡)
7572, 74fssd 5390 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}⟢𝐡)
76 simpl1 1001 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ Β¬ 𝑧 ∈ 𝑀)
77 disjsn 3666 . . . . . . . . . . . . . 14 ((𝑀 ∩ {𝑧}) = βˆ… ↔ Β¬ 𝑧 ∈ 𝑀)
7876, 77sylibr 134 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (𝑀 ∩ {𝑧}) = βˆ…)
79 fun2 5401 . . . . . . . . . . . . 13 (((𝑓:π‘€βŸΆπ΅ ∧ {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}⟢𝐡) ∧ (𝑀 ∩ {𝑧}) = βˆ…) β†’ (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡)
8068, 75, 78, 79syl21anc 1247 . . . . . . . . . . . 12 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡)
81 simprr 531 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆ€π‘₯ ∈ 𝑀 πœ“)
82 eleq1a 2259 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ 𝑀 β†’ (𝑧 = π‘₯ β†’ 𝑧 ∈ 𝑀))
8382necon3bd 2400 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ 𝑀 β†’ (Β¬ 𝑧 ∈ 𝑀 β†’ 𝑧 β‰  π‘₯))
8483impcom 125 . . . . . . . . . . . . . . . . 17 ((Β¬ 𝑧 ∈ 𝑀 ∧ π‘₯ ∈ 𝑀) β†’ 𝑧 β‰  π‘₯)
85 fvunsng 5723 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ V ∧ 𝑧 β‰  π‘₯) β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = (π‘“β€˜π‘₯))
8620, 85mpan 424 . . . . . . . . . . . . . . . . 17 (𝑧 β‰  π‘₯ β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = (π‘“β€˜π‘₯))
87 dfsbcq 2976 . . . . . . . . . . . . . . . . . 18 (((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = (π‘“β€˜π‘₯) β†’ ([((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘ ↔ [(π‘“β€˜π‘₯) / 𝑦]πœ‘))
8887, 23bitr2di 197 . . . . . . . . . . . . . . . . 17 (((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = (π‘“β€˜π‘₯) β†’ (πœ“ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
8984, 86, 883syl 17 . . . . . . . . . . . . . . . 16 ((Β¬ 𝑧 ∈ 𝑀 ∧ π‘₯ ∈ 𝑀) β†’ (πœ“ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
9089ralbidva 2483 . . . . . . . . . . . . . . 15 (Β¬ 𝑧 ∈ 𝑀 β†’ (βˆ€π‘₯ ∈ 𝑀 πœ“ ↔ βˆ€π‘₯ ∈ 𝑀 [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
9176, 90syl 14 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ 𝑀 πœ“ ↔ βˆ€π‘₯ ∈ 𝑀 [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
9281, 91mpbid 147 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆ€π‘₯ ∈ 𝑀 [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)
93 simpl3 1003 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ [𝑧 / π‘₯]πœ‘)
94 ffun 5380 . . . . . . . . . . . . . . . . 17 ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡 β†’ Fun (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}))
95 ssun2 3311 . . . . . . . . . . . . . . . . . 18 {βŸ¨π‘§, π‘¦βŸ©} βŠ† (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})
96 vsnid 3636 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ {𝑧}
9769dmsnop 5114 . . . . . . . . . . . . . . . . . . 19 dom {βŸ¨π‘§, π‘¦βŸ©} = {𝑧}
9896, 97eleqtrri 2263 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ dom {βŸ¨π‘§, π‘¦βŸ©}
99 funssfv 5553 . . . . . . . . . . . . . . . . . 18 ((Fun (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) ∧ {βŸ¨π‘§, π‘¦βŸ©} βŠ† (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) ∧ 𝑧 ∈ dom {βŸ¨π‘§, π‘¦βŸ©}) β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) = ({βŸ¨π‘§, π‘¦βŸ©}β€˜π‘§))
10095, 98, 99mp3an23 1339 . . . . . . . . . . . . . . . . 17 (Fun (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) = ({βŸ¨π‘§, π‘¦βŸ©}β€˜π‘§))
10180, 94, 1003syl 17 . . . . . . . . . . . . . . . 16 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) = ({βŸ¨π‘§, π‘¦βŸ©}β€˜π‘§))
10253, 69fvsn 5724 . . . . . . . . . . . . . . . 16 ({βŸ¨π‘§, π‘¦βŸ©}β€˜π‘§) = 𝑦
103101, 102eqtr2di 2237 . . . . . . . . . . . . . . 15 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ 𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§))
104 ralsnsg 3641 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V β†’ (βˆ€π‘₯ ∈ {𝑧}πœ‘ ↔ [𝑧 / π‘₯]πœ‘))
10553, 104ax-mp 5 . . . . . . . . . . . . . . . 16 (βˆ€π‘₯ ∈ {𝑧}πœ‘ ↔ [𝑧 / π‘₯]πœ‘)
106 elsni 3622 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ {𝑧} β†’ π‘₯ = 𝑧)
107106fveq2d 5531 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ {𝑧} β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§))
108107eqeq2d 2199 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ {𝑧} β†’ (𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) ↔ 𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§)))
109108biimparc 299 . . . . . . . . . . . . . . . . . 18 ((𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) ∧ π‘₯ ∈ {𝑧}) β†’ 𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯))
110 sbceq1a 2984 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) β†’ (πœ‘ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
111109, 110syl 14 . . . . . . . . . . . . . . . . 17 ((𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) ∧ π‘₯ ∈ {𝑧}) β†’ (πœ‘ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
112111ralbidva 2483 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) β†’ (βˆ€π‘₯ ∈ {𝑧}πœ‘ ↔ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
113105, 112bitr3id 194 . . . . . . . . . . . . . . 15 (𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) β†’ ([𝑧 / π‘₯]πœ‘ ↔ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
114103, 113syl 14 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ ([𝑧 / π‘₯]πœ‘ ↔ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
11593, 114mpbid 147 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)
116 ralun 3329 . . . . . . . . . . . . 13 ((βˆ€π‘₯ ∈ 𝑀 [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘ ∧ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘) β†’ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)
11792, 115, 116syl2anc 411 . . . . . . . . . . . 12 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)
11853, 69opex 4241 . . . . . . . . . . . . . . 15 βŸ¨π‘§, π‘¦βŸ© ∈ V
119118snex 4197 . . . . . . . . . . . . . 14 {βŸ¨π‘§, π‘¦βŸ©} ∈ V
12019, 119unex 4453 . . . . . . . . . . . . 13 (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) ∈ V
121 feq1 5360 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ (𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ↔ (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡))
122 fveq1 5526 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ (π‘”β€˜π‘₯) = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯))
123122sbceq1d 2979 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ ([(π‘”β€˜π‘₯) / 𝑦]πœ‘ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
124123ralbidv 2487 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘ ↔ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
125121, 124anbi12d 473 . . . . . . . . . . . . 13 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ ((𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘) ↔ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)))
126120, 125spcev 2844 . . . . . . . . . . . 12 (((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
12780, 117, 126syl2anc 411 . . . . . . . . . . 11 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
128127ex 115 . . . . . . . . . 10 ((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) β†’ ((𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))
129128exlimdv 1829 . . . . . . . . 9 ((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))
1301293exp 1203 . . . . . . . 8 (Β¬ 𝑧 ∈ 𝑀 β†’ (𝑦 ∈ 𝐡 β†’ ([𝑧 / π‘₯]πœ‘ β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))))
13159, 67, 130rexlimd 2601 . . . . . . 7 (Β¬ 𝑧 ∈ 𝑀 β†’ (βˆƒπ‘¦ ∈ 𝐡 [𝑧 / π‘₯]πœ‘ β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
13258, 131syl5 32 . . . . . 6 (Β¬ 𝑧 ∈ 𝑀 β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
133132a2d 26 . . . . 5 (Β¬ 𝑧 ∈ 𝑀 β†’ ((βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
13449, 133syl5 32 . . . 4 (Β¬ 𝑧 ∈ 𝑀 β†’ ((βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
135134adantl 277 . . 3 ((𝑀 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑀) β†’ ((βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
1366, 12, 31, 37, 45, 135findcard2s 6904 . 2 (𝐴 ∈ Fin β†’ (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“)))
137136imp 124 1 ((𝐴 ∈ Fin ∧ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐡 πœ‘) β†’ βˆƒπ‘“(𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“))
Colors of variables: wff set class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 979   = wceq 1363  βˆƒwex 1502   ∈ wcel 2158   β‰  wne 2357  βˆ€wral 2465  βˆƒwrex 2466  Vcvv 2749  [wsbc 2974   βˆͺ cun 3139   ∩ cin 3140   βŠ† wss 3141  βˆ…c0 3434  {csn 3604  βŸ¨cop 3607  dom cdm 4638  Fun wfun 5222  βŸΆwf 5224  β€“1-1-ontoβ†’wf1o 5227  β€˜cfv 5228  Fincfn 6754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-ral 2470  df-rex 2471  df-reu 2472  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-iord 4378  df-on 4380  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-er 6549  df-en 6755  df-fin 6757
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator