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

Theorem ac6sfi 6901
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 2673 . . . 4 (𝑒 = βˆ… β†’ (βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆ€π‘₯ ∈ βˆ… βˆƒπ‘¦ ∈ 𝐡 πœ‘))
2 feq2 5351 . . . . . 6 (𝑒 = βˆ… β†’ (𝑓:π‘’βŸΆπ΅ ↔ 𝑓:βˆ…βŸΆπ΅))
3 raleq 2673 . . . . . 6 (𝑒 = βˆ… β†’ (βˆ€π‘₯ ∈ 𝑒 πœ“ ↔ βˆ€π‘₯ ∈ βˆ… πœ“))
42, 3anbi12d 473 . . . . 5 (𝑒 = βˆ… β†’ ((𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ (𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“)))
54exbidv 1825 . . . 4 (𝑒 = βˆ… β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘“(𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“)))
61, 5imbi12d 234 . . 3 (𝑒 = βˆ… β†’ ((βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“)) ↔ (βˆ€π‘₯ ∈ βˆ… βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“))))
7 raleq 2673 . . . 4 (𝑒 = 𝑀 β†’ (βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘))
8 feq2 5351 . . . . . 6 (𝑒 = 𝑀 β†’ (𝑓:π‘’βŸΆπ΅ ↔ 𝑓:π‘€βŸΆπ΅))
9 raleq 2673 . . . . . 6 (𝑒 = 𝑀 β†’ (βˆ€π‘₯ ∈ 𝑒 πœ“ ↔ βˆ€π‘₯ ∈ 𝑀 πœ“))
108, 9anbi12d 473 . . . . 5 (𝑒 = 𝑀 β†’ ((𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)))
1110exbidv 1825 . . . 4 (𝑒 = 𝑀 β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)))
127, 11imbi12d 234 . . 3 (𝑒 = 𝑀 β†’ ((βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“)) ↔ (βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“))))
13 raleq 2673 . . . 4 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘))
14 feq2 5351 . . . . . . 7 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (𝑓:π‘’βŸΆπ΅ ↔ 𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡))
15 raleq 2673 . . . . . . 7 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (βˆ€π‘₯ ∈ 𝑒 πœ“ ↔ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“))
1614, 15anbi12d 473 . . . . . 6 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ ((𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ (𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“)))
1716exbidv 1825 . . . . 5 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘“(𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“)))
18 feq1 5350 . . . . . . 7 (𝑓 = 𝑔 β†’ (𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ↔ 𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡))
19 vex 2742 . . . . . . . . . . 11 𝑓 ∈ V
20 vex 2742 . . . . . . . . . . 11 π‘₯ ∈ V
2119, 20fvex 5537 . . . . . . . . . 10 (π‘“β€˜π‘₯) ∈ V
22 ac6sfi.1 . . . . . . . . . 10 (𝑦 = (π‘“β€˜π‘₯) β†’ (πœ‘ ↔ πœ“))
2321, 22sbcie 2999 . . . . . . . . 9 ([(π‘“β€˜π‘₯) / 𝑦]πœ‘ ↔ πœ“)
24 fveq1 5516 . . . . . . . . . 10 (𝑓 = 𝑔 β†’ (π‘“β€˜π‘₯) = (π‘”β€˜π‘₯))
2524sbceq1d 2969 . . . . . . . . 9 (𝑓 = 𝑔 β†’ ([(π‘“β€˜π‘₯) / 𝑦]πœ‘ ↔ [(π‘”β€˜π‘₯) / 𝑦]πœ‘))
2623, 25bitr3id 194 . . . . . . . 8 (𝑓 = 𝑔 β†’ (πœ“ ↔ [(π‘”β€˜π‘₯) / 𝑦]πœ‘))
2726ralbidv 2477 . . . . . . 7 (𝑓 = 𝑔 β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“ ↔ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
2818, 27anbi12d 473 . . . . . 6 (𝑓 = 𝑔 β†’ ((𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“) ↔ (𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))
2928cbvexv 1918 . . . . 5 (βˆƒπ‘“(𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“) ↔ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
3017, 29bitrdi 196 . . . 4 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))
3113, 30imbi12d 234 . . 3 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ ((βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“)) ↔ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
32 raleq 2673 . . . 4 (𝑒 = 𝐴 β†’ (βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐡 πœ‘))
33 feq2 5351 . . . . . 6 (𝑒 = 𝐴 β†’ (𝑓:π‘’βŸΆπ΅ ↔ 𝑓:𝐴⟢𝐡))
34 raleq 2673 . . . . . 6 (𝑒 = 𝐴 β†’ (βˆ€π‘₯ ∈ 𝑒 πœ“ ↔ βˆ€π‘₯ ∈ 𝐴 πœ“))
3533, 34anbi12d 473 . . . . 5 (𝑒 = 𝐴 β†’ ((𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ (𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“)))
3635exbidv 1825 . . . 4 (𝑒 = 𝐴 β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘“(𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“)))
3732, 36imbi12d 234 . . 3 (𝑒 = 𝐴 β†’ ((βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“)) ↔ (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“))))
38 f0 5408 . . . 4 βˆ…:βˆ…βŸΆπ΅
39 0ex 4132 . . . . 5 βˆ… ∈ V
40 ral0 3526 . . . . . . 7 βˆ€π‘₯ ∈ βˆ… πœ“
4140biantru 302 . . . . . 6 (𝑓:βˆ…βŸΆπ΅ ↔ (𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“))
42 feq1 5350 . . . . . 6 (𝑓 = βˆ… β†’ (𝑓:βˆ…βŸΆπ΅ ↔ βˆ…:βˆ…βŸΆπ΅))
4341, 42bitr3id 194 . . . . 5 (𝑓 = βˆ… β†’ ((𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“) ↔ βˆ…:βˆ…βŸΆπ΅))
4439, 43spcev 2834 . . . 4 (βˆ…:βˆ…βŸΆπ΅ β†’ βˆƒπ‘“(𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“))
4538, 44mp1i 10 . . 3 (βˆ€π‘₯ ∈ βˆ… βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“))
46 ssun1 3300 . . . . . . 7 𝑀 βŠ† (𝑀 βˆͺ {𝑧})
47 ssralv 3221 . . . . . . 7 (𝑀 βŠ† (𝑀 βˆͺ {𝑧}) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘))
4846, 47ax-mp 5 . . . . . 6 (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘)
4948imim1i 60 . . . . 5 ((βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)))
50 ssun2 3301 . . . . . . . . 9 {𝑧} βŠ† (𝑀 βˆͺ {𝑧})
51 ssralv 3221 . . . . . . . . 9 ({𝑧} βŠ† (𝑀 βˆͺ {𝑧}) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘))
5250, 51ax-mp 5 . . . . . . . 8 (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘)
53 vex 2742 . . . . . . . . . 10 𝑧 ∈ V
54 ralsnsg 3631 . . . . . . . . . 10 (𝑧 ∈ V β†’ (βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ [𝑧 / π‘₯]βˆƒπ‘¦ ∈ 𝐡 πœ‘))
5553, 54ax-mp 5 . . . . . . . . 9 (βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ [𝑧 / π‘₯]βˆƒπ‘¦ ∈ 𝐡 πœ‘)
56 sbcrex 3044 . . . . . . . . 9 ([𝑧 / π‘₯]βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆƒπ‘¦ ∈ 𝐡 [𝑧 / π‘₯]πœ‘)
5755, 56bitri 184 . . . . . . . 8 (βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆƒπ‘¦ ∈ 𝐡 [𝑧 / π‘₯]πœ‘)
5852, 57sylib 122 . . . . . . 7 (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘¦ ∈ 𝐡 [𝑧 / π‘₯]πœ‘)
59 nfv 1528 . . . . . . . 8 Ⅎ𝑦 Β¬ 𝑧 ∈ 𝑀
60 nfv 1528 . . . . . . . . 9 β„²π‘¦βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)
61 nfv 1528 . . . . . . . . . . 11 Ⅎ𝑦 𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡
62 nfcv 2319 . . . . . . . . . . . 12 Ⅎ𝑦(𝑀 βˆͺ {𝑧})
63 nfsbc1v 2983 . . . . . . . . . . . 12 Ⅎ𝑦[(π‘”β€˜π‘₯) / 𝑦]πœ‘
6462, 63nfralxy 2515 . . . . . . . . . . 11 β„²π‘¦βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘
6561, 64nfan 1565 . . . . . . . . . 10 Ⅎ𝑦(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)
6665nfex 1637 . . . . . . . . 9 β„²π‘¦βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)
6760, 66nfim 1572 . . . . . . . 8 Ⅎ𝑦(βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
68 simprl 529 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ 𝑓:π‘€βŸΆπ΅)
69 vex 2742 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
7053, 69f1osn 5503 . . . . . . . . . . . . . . 15 {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}–1-1-ontoβ†’{𝑦}
71 f1of 5463 . . . . . . . . . . . . . . 15 ({βŸ¨π‘§, π‘¦βŸ©}:{𝑧}–1-1-ontoβ†’{𝑦} β†’ {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}⟢{𝑦})
7270, 71mp1i 10 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}⟢{𝑦})
73 simpl2 1001 . . . . . . . . . . . . . . 15 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ 𝑦 ∈ 𝐡)
7473snssd 3739 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ {𝑦} βŠ† 𝐡)
7572, 74fssd 5380 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}⟢𝐡)
76 simpl1 1000 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ Β¬ 𝑧 ∈ 𝑀)
77 disjsn 3656 . . . . . . . . . . . . . 14 ((𝑀 ∩ {𝑧}) = βˆ… ↔ Β¬ 𝑧 ∈ 𝑀)
7876, 77sylibr 134 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (𝑀 ∩ {𝑧}) = βˆ…)
79 fun2 5391 . . . . . . . . . . . . 13 (((𝑓:π‘€βŸΆπ΅ ∧ {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}⟢𝐡) ∧ (𝑀 ∩ {𝑧}) = βˆ…) β†’ (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡)
8068, 75, 78, 79syl21anc 1237 . . . . . . . . . . . 12 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡)
81 simprr 531 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆ€π‘₯ ∈ 𝑀 πœ“)
82 eleq1a 2249 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ 𝑀 β†’ (𝑧 = π‘₯ β†’ 𝑧 ∈ 𝑀))
8382necon3bd 2390 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ 𝑀 β†’ (Β¬ 𝑧 ∈ 𝑀 β†’ 𝑧 β‰  π‘₯))
8483impcom 125 . . . . . . . . . . . . . . . . 17 ((Β¬ 𝑧 ∈ 𝑀 ∧ π‘₯ ∈ 𝑀) β†’ 𝑧 β‰  π‘₯)
85 fvunsng 5713 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ V ∧ 𝑧 β‰  π‘₯) β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = (π‘“β€˜π‘₯))
8620, 85mpan 424 . . . . . . . . . . . . . . . . 17 (𝑧 β‰  π‘₯ β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = (π‘“β€˜π‘₯))
87 dfsbcq 2966 . . . . . . . . . . . . . . . . . 18 (((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = (π‘“β€˜π‘₯) β†’ ([((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘ ↔ [(π‘“β€˜π‘₯) / 𝑦]πœ‘))
8887, 23bitr2di 197 . . . . . . . . . . . . . . . . 17 (((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = (π‘“β€˜π‘₯) β†’ (πœ“ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
8984, 86, 883syl 17 . . . . . . . . . . . . . . . 16 ((Β¬ 𝑧 ∈ 𝑀 ∧ π‘₯ ∈ 𝑀) β†’ (πœ“ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
9089ralbidva 2473 . . . . . . . . . . . . . . 15 (Β¬ 𝑧 ∈ 𝑀 β†’ (βˆ€π‘₯ ∈ 𝑀 πœ“ ↔ βˆ€π‘₯ ∈ 𝑀 [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
9176, 90syl 14 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ 𝑀 πœ“ ↔ βˆ€π‘₯ ∈ 𝑀 [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
9281, 91mpbid 147 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆ€π‘₯ ∈ 𝑀 [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)
93 simpl3 1002 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ [𝑧 / π‘₯]πœ‘)
94 ffun 5370 . . . . . . . . . . . . . . . . 17 ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡 β†’ Fun (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}))
95 ssun2 3301 . . . . . . . . . . . . . . . . . 18 {βŸ¨π‘§, π‘¦βŸ©} βŠ† (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})
96 vsnid 3626 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ {𝑧}
9769dmsnop 5104 . . . . . . . . . . . . . . . . . . 19 dom {βŸ¨π‘§, π‘¦βŸ©} = {𝑧}
9896, 97eleqtrri 2253 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ dom {βŸ¨π‘§, π‘¦βŸ©}
99 funssfv 5543 . . . . . . . . . . . . . . . . . 18 ((Fun (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) ∧ {βŸ¨π‘§, π‘¦βŸ©} βŠ† (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) ∧ 𝑧 ∈ dom {βŸ¨π‘§, π‘¦βŸ©}) β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) = ({βŸ¨π‘§, π‘¦βŸ©}β€˜π‘§))
10095, 98, 99mp3an23 1329 . . . . . . . . . . . . . . . . 17 (Fun (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) = ({βŸ¨π‘§, π‘¦βŸ©}β€˜π‘§))
10180, 94, 1003syl 17 . . . . . . . . . . . . . . . 16 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) = ({βŸ¨π‘§, π‘¦βŸ©}β€˜π‘§))
10253, 69fvsn 5714 . . . . . . . . . . . . . . . 16 ({βŸ¨π‘§, π‘¦βŸ©}β€˜π‘§) = 𝑦
103101, 102eqtr2di 2227 . . . . . . . . . . . . . . 15 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ 𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§))
104 ralsnsg 3631 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V β†’ (βˆ€π‘₯ ∈ {𝑧}πœ‘ ↔ [𝑧 / π‘₯]πœ‘))
10553, 104ax-mp 5 . . . . . . . . . . . . . . . 16 (βˆ€π‘₯ ∈ {𝑧}πœ‘ ↔ [𝑧 / π‘₯]πœ‘)
106 elsni 3612 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ {𝑧} β†’ π‘₯ = 𝑧)
107106fveq2d 5521 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ {𝑧} β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§))
108107eqeq2d 2189 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ {𝑧} β†’ (𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) ↔ 𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§)))
109108biimparc 299 . . . . . . . . . . . . . . . . . 18 ((𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) ∧ π‘₯ ∈ {𝑧}) β†’ 𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯))
110 sbceq1a 2974 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) β†’ (πœ‘ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
111109, 110syl 14 . . . . . . . . . . . . . . . . 17 ((𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) ∧ π‘₯ ∈ {𝑧}) β†’ (πœ‘ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
112111ralbidva 2473 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) β†’ (βˆ€π‘₯ ∈ {𝑧}πœ‘ ↔ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
113105, 112bitr3id 194 . . . . . . . . . . . . . . 15 (𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) β†’ ([𝑧 / π‘₯]πœ‘ ↔ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
114103, 113syl 14 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ ([𝑧 / π‘₯]πœ‘ ↔ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
11593, 114mpbid 147 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)
116 ralun 3319 . . . . . . . . . . . . 13 ((βˆ€π‘₯ ∈ 𝑀 [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘ ∧ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘) β†’ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)
11792, 115, 116syl2anc 411 . . . . . . . . . . . 12 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)
11853, 69opex 4231 . . . . . . . . . . . . . . 15 βŸ¨π‘§, π‘¦βŸ© ∈ V
119118snex 4187 . . . . . . . . . . . . . 14 {βŸ¨π‘§, π‘¦βŸ©} ∈ V
12019, 119unex 4443 . . . . . . . . . . . . 13 (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) ∈ V
121 feq1 5350 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ (𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ↔ (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡))
122 fveq1 5516 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ (π‘”β€˜π‘₯) = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯))
123122sbceq1d 2969 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ ([(π‘”β€˜π‘₯) / 𝑦]πœ‘ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
124123ralbidv 2477 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘ ↔ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
125121, 124anbi12d 473 . . . . . . . . . . . . 13 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ ((𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘) ↔ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)))
126120, 125spcev 2834 . . . . . . . . . . . 12 (((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
12780, 117, 126syl2anc 411 . . . . . . . . . . 11 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
128127ex 115 . . . . . . . . . 10 ((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) β†’ ((𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))
129128exlimdv 1819 . . . . . . . . 9 ((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))
1301293exp 1202 . . . . . . . 8 (Β¬ 𝑧 ∈ 𝑀 β†’ (𝑦 ∈ 𝐡 β†’ ([𝑧 / π‘₯]πœ‘ β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))))
13159, 67, 130rexlimd 2591 . . . . . . 7 (Β¬ 𝑧 ∈ 𝑀 β†’ (βˆƒπ‘¦ ∈ 𝐡 [𝑧 / π‘₯]πœ‘ β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
13258, 131syl5 32 . . . . . 6 (Β¬ 𝑧 ∈ 𝑀 β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
133132a2d 26 . . . . 5 (Β¬ 𝑧 ∈ 𝑀 β†’ ((βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
13449, 133syl5 32 . . . 4 (Β¬ 𝑧 ∈ 𝑀 β†’ ((βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
135134adantl 277 . . 3 ((𝑀 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑀) β†’ ((βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
1366, 12, 31, 37, 45, 135findcard2s 6893 . 2 (𝐴 ∈ Fin β†’ (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“)))
137136imp 124 1 ((𝐴 ∈ Fin ∧ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐡 πœ‘) β†’ βˆƒπ‘“(𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“))
Colors of variables: wff set class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 978   = wceq 1353  βˆƒwex 1492   ∈ wcel 2148   β‰  wne 2347  βˆ€wral 2455  βˆƒwrex 2456  Vcvv 2739  [wsbc 2964   βˆͺ cun 3129   ∩ cin 3130   βŠ† wss 3131  βˆ…c0 3424  {csn 3594  βŸ¨cop 3597  dom cdm 4628  Fun wfun 5212  βŸΆwf 5214  β€“1-1-ontoβ†’wf1o 5217  β€˜cfv 5218  Fincfn 6743
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-if 3537  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-iord 4368  df-on 4370  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-er 6538  df-en 6744  df-fin 6746
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator